|
Static Value-Flow Analysis
|
Go to the source code of this file.
Classes | |
| struct | cuddPathPair |
| union | hack |
Macros | |
| #define | BETA 0.6 |
| #define | ALPHA 0.90 |
| #define | EXC_PROB 0.4 |
| #define | JUMP_UP_PROB 0.36 |
| #define | MAXGEN_RATIO 15.0 |
| #define | STOP_TEMP 1.0 |
| #define | STOREDD(i, j) storedd[(i)*(numvars+1)+(j)] |
| #define | DD_NORMAL_SIFT 0 |
| #define | DD_LAZY_SIFT 1 |
| #define | DD_SIFT_DOWN 0 |
| #define | DD_SIFT_UP 1 |
| #define | BPL 32 |
| #define | LOGBPL 5 |
| #define | DD_MAX_HASHTABLE_DENSITY 2 /* tells when to resize a table */ |
| #define | ddLCHash1(f, shift) (((unsigned)(f) * DD_P1) >> (shift)) |
| #define | ddLCHash2(f, g, shift) ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (shift)) |
| #define | ddLCHash3(f, g, h, shift) ddCHash2(f,g,h,shift) |
| #define | CUDD_SWAP_MOVE 0 |
| #define | CUDD_LINEAR_TRANSFORM_MOVE 1 |
| #define | CUDD_INVERSE_TRANSFORM_MOVE 2 |
| #define | BPL 32 |
| #define | LOGBPL 5 |
| #define | DD_MAX_SUBTABLE_SPARSITY 8 |
| #define | DD_BIGGY 100000000 |
| #define | WEIGHT(weight, col) ((weight) == NULL ? 1 : weight[col]) |
| #define | MV_OOM (Move *)1 |
| #define | MODULUS1 2147483563 |
| #define | LEQA1 40014 |
| #define | LEQQ1 53668 |
| #define | LEQR1 12211 |
| #define | MODULUS2 2147483399 |
| #define | LEQA2 40692 |
| #define | LEQQ2 52774 |
| #define | LEQR2 3791 |
| #define | STAB_SIZE 64 |
| #define | STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE) |
| #define | bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ') |
| #define | ABC 1 |
| #define | BAC 2 |
| #define | BCA 3 |
| #define | CBA 4 |
| #define | CAB 5 |
| #define | ACB 6 |
| #define | ABCD 1 |
| #define | BACD 7 |
| #define | BADC 13 |
| #define | ABDC 8 |
| #define | ADBC 14 |
| #define | ADCB 9 |
| #define | DACB 15 |
| #define | DABC 20 |
| #define | DBAC 23 |
| #define | BDAC 19 |
| #define | BDCA 21 |
| #define | DBCA 24 |
| #define | DCBA 22 |
| #define | DCAB 18 |
| #define | CDAB 12 |
| #define | CDBA 17 |
| #define | CBDA 11 |
| #define | BCDA 16 |
| #define | BCAD 10 |
| #define | CBAD 5 |
| #define | CABD 3 |
| #define | CADB 6 |
| #define | ACDB 4 |
| #define | ACBD 2 |
| #define | CUDD_SWAP_MOVE 0 |
| #define | CUDD_LINEAR_TRANSFORM_MOVE 1 |
| #define | CUDD_INVERSE_TRANSFORM_MOVE 2 |
| #define | DD_MAX_SUBTABLE_SPARSITY 8 |
| #define | ZDD_MV_OOM (Move *)1 |
Typedefs | |
| typedef int(* | DD_CHKFP) (DdManager *, int, int) |
| typedef struct cuddPathPair | cuddPathPair |
| typedef union hack | hack |
Functions | |
| static void | addVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero) |
| DdNode * | Cudd_addIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
| DdNode * | Cudd_addEvalConst (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | Cudd_addCmpl (DdManager *dd, DdNode *f) |
| int | Cudd_addLeq (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | cuddAddIteRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
| DdNode * | cuddAddCmplRecur (DdManager *dd, DdNode *f) |
| static int | stopping_criterion (int c1, int c2, int c3, int c4, double temp) |
| static double | random_generator (void) |
| static int | ddExchange (DdManager *table, int x, int y, double temp) |
| static int | ddJumpingAux (DdManager *table, int x, int x_low, int x_high, double temp) |
| static Move * | ddJumpingUp (DdManager *table, int x, int x_low, int initial_size) |
| static Move * | ddJumpingDown (DdManager *table, int x, int x_high, int initial_size) |
| static int | siftBackwardProb (DdManager *table, Move *moves, int size, double temp) |
| static void | copyOrder (DdManager *table, int *array, int lower, int upper) |
| static int | restoreOrder (DdManager *table, int *array, int lower, int upper) |
| int | cuddAnnealing (DdManager *table, int lower, int upper) |
| static void | fixVarTree (MtrNode *treenode, int *perm, int size) |
| static int | addMultiplicityGroups (DdManager *dd, MtrNode *treenode, int multiplicity, char *vmask, char *lmask) |
| DdNode * | Cudd_bddIthVar (DdManager *dd, int i) |
| DdNode * | Cudd_ReadOne (DdManager *dd) |
| DdNode * | Cudd_ReadLogicZero (DdManager *dd) |
| void | Cudd_SetMinHit (DdManager *dd, unsigned int hr) |
| int | Cudd_ReadSize (DdManager *dd) |
| void | Cudd_FreeTree (DdManager *dd) |
| void | Cudd_FreeZddTree (DdManager *dd) |
| int | Cudd_ReadPerm (DdManager *dd, int i) |
| CUDD_VALUE_TYPE | Cudd_ReadEpsilon (DdManager *dd) |
| void | Cudd_SetEpsilon (DdManager *dd, CUDD_VALUE_TYPE ep) |
| unsigned long | Cudd_ReadMemoryInUse (DdManager *dd) |
| long | Cudd_ReadNodeCount (DdManager *dd) |
| int | Cudd_RemoveHook (DdManager *dd, DD_HFP f, Cudd_HookType where) |
| int | Cudd_bddReadPairIndex (DdManager *dd, int index) |
| int | Cudd_bddIsVarToBeGrouped (DdManager *dd, int index) |
| int | Cudd_bddIsVarToBeUngrouped (DdManager *dd, int index) |
| static int | bddCheckPositiveCube (DdManager *manager, DdNode *cube) |
| DdNode * | Cudd_bddExistAbstract (DdManager *manager, DdNode *f, DdNode *cube) |
| int | Cudd_bddVarIsDependent (DdManager *dd, DdNode *f, DdNode *var) |
| DdNode * | cuddBddExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube) |
| DdNode * | cuddBddXorExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube) |
| DdNode * | cuddBddBooleanDiffRecur (DdManager *manager, DdNode *f, DdNode *var) |
| static void | bddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one) |
| static int | bddVarToCanonical (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp) |
| static int | bddVarToCanonicalSimple (DdManager *dd, DdNode **fp, DdNode **gp, DdNode **hp, unsigned int *topfp, unsigned int *topgp, unsigned int *tophp) |
| DdNode * | Cudd_bddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
| DdNode * | Cudd_bddIteConstant (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
| DdNode * | Cudd_bddIntersect (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | Cudd_bddAnd (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | Cudd_bddAndLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit) |
| DdNode * | Cudd_bddOr (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | Cudd_bddOrLimit (DdManager *dd, DdNode *f, DdNode *g, unsigned int limit) |
| DdNode * | Cudd_bddXor (DdManager *dd, DdNode *f, DdNode *g) |
| int | Cudd_bddLeq (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | cuddBddIteRecur (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
| DdNode * | cuddBddIntersectRecur (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | cuddBddAndRecur (DdManager *manager, DdNode *f, DdNode *g) |
| DdNode * | cuddBddXorRecur (DdManager *manager, DdNode *f, DdNode *g) |
| int | cuddInitCache (DdManager *unique, unsigned int cacheSize, unsigned int maxCacheSize) |
| void | cuddCacheInsert (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h, DdNode *data) |
| void | cuddCacheInsert2 (DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data) |
| void | cuddCacheInsert1 (DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data) |
| DdNode * | cuddCacheLookup (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h) |
| DdNode * | cuddCacheLookupZdd (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h) |
| DdNode * | cuddCacheLookup2 (DdManager *table, DD_CTFP op, DdNode *f, DdNode *g) |
| DdNode * | cuddCacheLookup1 (DdManager *table, DD_CTFP1 op, DdNode *f) |
| DdNode * | cuddCacheLookup2Zdd (DdManager *table, DD_CTFP op, DdNode *f, DdNode *g) |
| DdNode * | cuddCacheLookup1Zdd (DdManager *table, DD_CTFP1 op, DdNode *f) |
| DdNode * | cuddConstantLookup (DdManager *table, ptruint op, DdNode *f, DdNode *g, DdNode *h) |
| int | cuddCacheProfile (DdManager *table, FILE *fp) |
| void | cuddCacheResize (DdManager *table) |
| void | cuddCacheFlush (DdManager *table) |
| int | cuddComputeFloorLog2 (unsigned int value) |
| static void | debugFindParent (DdManager *table, DdNode *node) |
| int | Cudd_DebugCheck (DdManager *table) |
| int | Cudd_CheckKeys (DdManager *table) |
| int | cuddHeapProfile (DdManager *dd) |
| void | cuddPrintNode (DdNode *f, FILE *fp) |
| void | cuddPrintVarGroups (DdManager *dd, MtrNode *root, int zdd, int silent) |
| DdNode * | Cudd_Cofactor (DdManager *dd, DdNode *f, DdNode *g) |
| int | Cudd_CheckCube (DdManager *dd, DdNode *g) |
| void | cuddGetBranches (DdNode *g, DdNode **g1, DdNode **g0) |
| DdNode * | cuddCofactorRecur (DdManager *dd, DdNode *f, DdNode *g) |
| static int | getMaxBinomial (int n) |
| static DdHalfWord ** | getMatrix (int rows, int cols) |
| static void | freeMatrix (DdHalfWord **matrix) |
| static int | getLevelKeys (DdManager *table, int l) |
| static int | ddShuffle (DdManager *table, DdHalfWord *permutation, int lower, int upper) |
| static int | ddSiftUp (DdManager *table, int x, int xLow) |
| static int | updateUB (DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper) |
| static int | ddCountRoots (DdManager *table, int lower, int upper) |
| static void | ddClearGlobal (DdManager *table, int lower, int maxlevel) |
| static int | computeLB (DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level) |
| static int | updateEntry (DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper) |
| static void | pushDown (DdHalfWord *order, int j, int level) |
| static DdHalfWord * | initSymmInfo (DdManager *table, int lower, int upper) |
| static int | checkSymmInfo (DdManager *table, DdHalfWord *symmInfo, int index, int level) |
| int | cuddExact (DdManager *table, int lower, int upper) |
| static int | make_random (DdManager *table, int lower) |
| static int | sift_up (DdManager *table, int x, int x_low) |
| static int | build_dd (DdManager *table, int num, int lower, int upper) |
| static int | largest (void) |
| static int | rand_int (int a) |
| static int | array_hash (char *array, int modulus) |
| static int | array_compare (const char *array1, const char *array2) |
| static int | find_best (void) |
| static int | PMX (int maxvar) |
| static int | roulette (int *p1, int *p2) |
| int | cuddGa (DdManager *table, int lower, int upper) |
| static int | ddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method) |
| static int | ddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method) |
| static void | ddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper) |
| static int | ddUniqueCompareGroup (int *ptrX, int *ptrY) |
| static int | ddGroupSifting (DdManager *table, int lower, int upper, DD_CHKFP checkFunction, int lazyFlag) |
| static void | ddCreateGroup (DdManager *table, int x, int y) |
| static int | ddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh, DD_CHKFP checkFunction, int lazyFlag) |
| static int | ddGroupSiftingUp (DdManager *table, int y, int xLow, DD_CHKFP checkFunction, Move **moves) |
| static int | ddGroupSiftingDown (DdManager *table, int x, int xHigh, DD_CHKFP checkFunction, Move **moves) |
| static int | ddGroupMove (DdManager *table, int x, int y, Move **moves) |
| static int | ddGroupMoveBackward (DdManager *table, int x, int y) |
| static int | ddGroupSiftingBackward (DdManager *table, Move *moves, int size, int upFlag, int lazyFlag) |
| static void | ddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high) |
| static void | ddDissolveGroup (DdManager *table, int x, int y) |
| static int | ddNoCheck (DdManager *table, int x, int y) |
| static int | ddSecDiffCheck (DdManager *table, int x, int y) |
| static int | ddExtSymmCheck (DdManager *table, int x, int y) |
| static int | ddVarGroupCheck (DdManager *table, int x, int y) |
| static int | ddSetVarHandled (DdManager *dd, int index) |
| static int | ddResetVarHandled (DdManager *dd, int index) |
| static int | ddIsVarHandled (DdManager *dd, int index) |
| int | cuddTreeSifting (DdManager *table, Cudd_ReorderingType method) |
| DdManager * | Cudd_Init (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory) |
| void | Cudd_Quit (DdManager *unique) |
| int | cuddZddInitUniv (DdManager *zdd) |
| void | cuddZddFreeUniv (DdManager *zdd) |
| static void | ddSuppInteract (DdNode *f, char *support) |
| static void | ddClearLocal (DdNode *f) |
| static void | ddUpdateInteract (DdManager *table, char *support) |
| static void | ddClearGlobal2 (DdManager *table) |
| void | cuddSetInteract (DdManager *table, int x, int y) |
| int | cuddTestInteract (DdManager *table, int x, int y) |
| int | cuddInitInteract (DdManager *table) |
| static void | cuddLocalCacheResize (DdLocalCache *cache) |
| static DD_INLINE unsigned int | ddLCHash (DdNodePtr *key, unsigned int keysize, int shift) |
| static void | cuddLocalCacheAddToList (DdLocalCache *cache) |
| static void | cuddLocalCacheRemoveFromList (DdLocalCache *cache) |
| static int | cuddHashTableResize (DdHashTable *hash) |
| static DD_INLINE DdHashItem * | cuddHashTableAlloc (DdHashTable *hash) |
| void | cuddLocalCacheClearDead (DdManager *manager) |
| void | cuddLocalCacheClearAll (DdManager *manager) |
| DdHashTable * | cuddHashTableInit (DdManager *manager, unsigned int keySize, unsigned int initSize) |
| void | cuddHashTableQuit (DdHashTable *hash) |
| void | cuddHashTableGenericQuit (DdHashTable *hash) |
| int | cuddHashTableInsert (DdHashTable *hash, DdNodePtr *key, DdNode *value, ptrint count) |
| DdNode * | cuddHashTableLookup (DdHashTable *hash, DdNodePtr *key) |
| int | cuddHashTableInsert1 (DdHashTable *hash, DdNode *f, DdNode *value, ptrint count) |
| DdNode * | cuddHashTableLookup1 (DdHashTable *hash, DdNode *f) |
| int | cuddHashTableGenericInsert (DdHashTable *hash, DdNode *f, void *value) |
| void * | cuddHashTableGenericLookup (DdHashTable *hash, DdNode *f) |
| int | cuddHashTableInsert2 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *value, ptrint count) |
| DdNode * | cuddHashTableLookup2 (DdHashTable *hash, DdNode *f, DdNode *g) |
| int | cuddHashTableInsert3 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h, DdNode *value, ptrint count) |
| DdNode * | cuddHashTableLookup3 (DdHashTable *hash, DdNode *f, DdNode *g, DdNode *h) |
| static int | ddLinearUniqueCompare (int *ptrX, int *ptrY) |
| static int | ddLinearAndSiftingAux (DdManager *table, int x, int xLow, int xHigh) |
| static Move * | ddLinearAndSiftingUp (DdManager *table, int y, int xLow, Move *prevMoves) |
| static Move * | ddLinearAndSiftingDown (DdManager *table, int x, int xHigh, Move *prevMoves) |
| static int | ddLinearAndSiftingBackward (DdManager *table, int size, Move *moves) |
| static Move * | ddUndoMoves (DdManager *table, Move *moves) |
| static void | cuddXorLinear (DdManager *table, int x, int y) |
| int | Cudd_PrintLinear (DdManager *table) |
| int | cuddLinearAndSifting (DdManager *table, int lower, int upper) |
| int | cuddLinearInPlace (DdManager *table, int x, int y) |
| void | cuddUpdateInteractionMatrix (DdManager *table, int xindex, int yindex) |
| int | cuddInitLinear (DdManager *table) |
| int | cuddResizeLinear (DdManager *table) |
| void | Cudd_Ref (DdNode *n) |
| void | Cudd_RecursiveDeref (DdManager *table, DdNode *n) |
| void | Cudd_IterDerefBdd (DdManager *table, DdNode *n) |
| void | Cudd_RecursiveDerefZdd (DdManager *table, DdNode *n) |
| void | Cudd_Deref (DdNode *node) |
| void | cuddReclaim (DdManager *table, DdNode *n) |
| void | cuddReclaimZdd (DdManager *table, DdNode *n) |
| void | cuddShrinkDeathRow (DdManager *table) |
| void | cuddClearDeathRow (DdManager *table) |
| static int | ddUniqueCompare (int *ptrX, int *ptrY) |
| static Move * | ddSwapAny (DdManager *table, int x, int y) |
| static int | ddSiftingAux (DdManager *table, int x, int xLow, int xHigh) |
| static Move * | ddSiftingUp (DdManager *table, int y, int xLow) |
| static Move * | ddSiftingDown (DdManager *table, int x, int xHigh) |
| static int | ddSiftingBackward (DdManager *table, int size, Move *moves) |
| static int | ddReorderPreprocess (DdManager *table) |
| static int | ddReorderPostprocess (DdManager *table) |
| static int | ddShuffle2 (DdManager *table, int *permutation) |
| static int | ddSiftUp2 (DdManager *table, int x, int xLow) |
| static void | bddFixTree (DdManager *table, MtrNode *treenode) |
| static int | ddUpdateMtrTree (DdManager *table, MtrNode *treenode, int *perm, int *invperm) |
| static int | ddCheckPermuation (DdManager *table, MtrNode *treenode, int *perm, int *invperm) |
| int | Cudd_ReduceHeap (DdManager *table, Cudd_ReorderingType heuristic, int minsize) |
| DdNode * | cuddDynamicAllocNode (DdManager *table) |
| int | cuddSifting (DdManager *table, int lower, int upper) |
| int | cuddSwapping (DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic) |
| int | cuddNextHigh (DdManager *table, int x) |
| int | cuddNextLow (DdManager *table, int x) |
| int | cuddSwapInPlace (DdManager *table, int x, int y) |
| int | cuddBddAlignToZdd (DdManager *table) |
| static enum st_retval | freePathPair (char *key, char *value, char *arg) |
| static cuddPathPair | getShortest (DdNode *root, int *cost, int *support, st_table *visited) |
| static cuddPathPair | getLargest (DdNode *root, st_table *visited) |
| static DdNode * | getCube (DdManager *manager, st_table *visited, DdNode *f, int cost) |
| static DdNode * | ddBddMaximallyExpand (DdManager *dd, DdNode *lb, DdNode *ub, DdNode *f) |
| static int | ddBddShortestPathUnate (DdManager *dd, DdNode *f, int *phases, st_table *table) |
| DdNode * | Cudd_LargestCube (DdManager *manager, DdNode *f, int *length) |
| DdNode * | Cudd_Decreasing (DdManager *dd, DdNode *f, int i) |
| int | Cudd_EquivDC (DdManager *dd, DdNode *F, DdNode *G, DdNode *D) |
| int | Cudd_bddLeqUnless (DdManager *dd, DdNode *f, DdNode *g, DdNode *D) |
| int | Cudd_EqualSupNorm (DdManager *dd, DdNode *f, DdNode *g, CUDD_VALUE_TYPE tolerance, int pr) |
| DdNode * | Cudd_bddMakePrime (DdManager *dd, DdNode *cube, DdNode *f) |
| DdNode * | cuddBddMakePrime (DdManager *dd, DdNode *cube, DdNode *f) |
| static int | ddSymmUniqueCompare (int *ptrX, int *ptrY) |
| static int | ddSymmSiftingAux (DdManager *table, int x, int xLow, int xHigh) |
| static int | ddSymmSiftingConvAux (DdManager *table, int x, int xLow, int xHigh) |
| static Move * | ddSymmSiftingUp (DdManager *table, int y, int xLow) |
| static Move * | ddSymmSiftingDown (DdManager *table, int x, int xHigh) |
| static int | ddSymmGroupMove (DdManager *table, int x, int y, Move **moves) |
| static int | ddSymmGroupMoveBackward (DdManager *table, int x, int y) |
| static int | ddSymmSiftingBackward (DdManager *table, Move *moves, int size) |
| static void | ddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups) |
| int | cuddSymmCheck (DdManager *table, int x, int y) |
| int | cuddSymmSifting (DdManager *table, int lower, int upper) |
| int | cuddSymmSiftingConv (DdManager *table, int lower, int upper) |
| static void | ddRehashZdd (DdManager *unique, int i) |
| static int | ddResizeTable (DdManager *unique, int index, int amount) |
| static DD_INLINE void | ddFixLimits (DdManager *unique) |
| static void | ddPatchTree (DdManager *dd, MtrNode *treenode) |
| static void | ddReportRefMess (DdManager *unique, int i, const char *caller) |
| DdNode * | cuddAllocNode (DdManager *unique) |
| DdManager * | cuddInitTable (unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo) |
| void | cuddFreeTable (DdManager *unique) |
| int | cuddGarbageCollect (DdManager *unique, int clearCache) |
| DdNode * | cuddZddGetNode (DdManager *zdd, int id, DdNode *T, DdNode *E) |
| DdNode * | cuddZddGetNodeIVO (DdManager *dd, int index, DdNode *g, DdNode *h) |
| DdNode * | cuddUniqueInter (DdManager *unique, int index, DdNode *T, DdNode *E) |
| DdNode * | cuddUniqueInterIVO (DdManager *unique, int index, DdNode *T, DdNode *E) |
| DdNode * | cuddUniqueInterZdd (DdManager *unique, int index, DdNode *T, DdNode *E) |
| DdNode * | cuddUniqueConst (DdManager *unique, CUDD_VALUE_TYPE value) |
| void | cuddRehash (DdManager *unique, int i) |
| int | cuddResizeTableZdd (DdManager *unique, int index) |
| void | cuddSlowTableGrowth (DdManager *unique) |
| static int | dp2 (DdManager *dd, DdNode *f, st_table *t) |
| static void | ddPrintMintermAux (DdManager *dd, DdNode *node, int *list) |
| static int | ddDagInt (DdNode *n) |
| static int | cuddNodeArrayRecur (DdNode *f, DdNodePtr *table, int index) |
| static int | cuddEstimateCofactor (DdManager *dd, st_table *table, DdNode *node, int i, int phase, DdNode **ptr) |
| static DdNode * | cuddUniqueLookup (DdManager *unique, int index, DdNode *T, DdNode *E) |
| static int | cuddEstimateCofactorSimple (DdNode *node, int i) |
| static double | ddCountMintermAux (DdNode *node, double max, DdHashTable *table) |
| static int | ddEpdCountMintermAux (DdNode *node, EpDouble *max, EpDouble *epd, st_table *table) |
| static double | ddCountPathAux (DdNode *node, st_table *table) |
| static double | ddCountPathsToNonZero (DdNode *N, st_table *table) |
| static void | ddSupportStep (DdNode *f, int *support) |
| static void | ddClearFlag (DdNode *f) |
| static int | ddLeavesInt (DdNode *n) |
| static int | ddPickArbitraryMinterms (DdManager *dd, DdNode *node, int nvars, int nminterms, char **string) |
| static void | ddFindSupport (DdManager *dd, DdNode *f, int *SP) |
| double | Cudd_CountMinterm (DdManager *manager, DdNode *node, int nvars) |
| DdGen * | Cudd_FirstCube (DdManager *dd, DdNode *f, int **cube, CUDD_VALUE_TYPE *value) |
| int | Cudd_NextCube (DdGen *gen, int **cube, CUDD_VALUE_TYPE *value) |
| DdGen * | Cudd_FirstPrime (DdManager *dd, DdNode *l, DdNode *u, int **cube) |
| int | Cudd_NextPrime (DdGen *gen, int **cube) |
| int | Cudd_BddToCubeArray (DdManager *dd, DdNode *cube, int *array) |
| DdGen * | Cudd_FirstNode (DdManager *dd, DdNode *f, DdNode **node) |
| int | Cudd_NextNode (DdGen *gen, DdNode **node) |
| int | Cudd_GenFree (DdGen *gen) |
| int | Cudd_IsGenEmpty (DdGen *gen) |
| long | Cudd_Random (void) |
| void | Cudd_Srandom (long seed) |
| void | Cudd_OutOfMem (long size) |
| int | cuddCollectNodes (DdNode *f, st_table *visited) |
| DdNodePtr * | cuddNodeArray (DdNode *f, int *n) |
| static int | ddWindow2 (DdManager *table, int low, int high) |
| static int | ddWindowConv2 (DdManager *table, int low, int high) |
| static int | ddPermuteWindow3 (DdManager *table, int x) |
| static int | ddWindow3 (DdManager *table, int low, int high) |
| static int | ddWindowConv3 (DdManager *table, int low, int high) |
| static int | ddPermuteWindow4 (DdManager *table, int w) |
| static int | ddWindow4 (DdManager *table, int low, int high) |
| static int | ddWindowConv4 (DdManager *table, int low, int high) |
| int | cuddWindowReorder (DdManager *table, int low, int high, Cudd_ReorderingType submethod) |
| DdNode * | cuddZddProduct (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | cuddZddUnateProduct (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | cuddZddWeakDiv (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | cuddZddWeakDivF (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | cuddZddDivide (DdManager *dd, DdNode *f, DdNode *g) |
| DdNode * | cuddZddDivideF (DdManager *dd, DdNode *f, DdNode *g) |
| int | cuddZddGetCofactors3 (DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd) |
| int | cuddZddGetCofactors2 (DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0) |
| DdNode * | cuddZddComplement (DdManager *dd, DdNode *node) |
| int | cuddZddGetPosVarIndex (DdManager *dd, int index) |
| int | cuddZddGetNegVarIndex (DdManager *dd, int index) |
| int | cuddZddGetPosVarLevel (DdManager *dd, int index) |
| int | cuddZddGetNegVarLevel (DdManager *dd, int index) |
| static int | zddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method) |
| static int | zddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method) |
| static void | zddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper) |
| static int | zddUniqueCompareGroup (int *ptrX, int *ptrY) |
| static int | zddGroupSifting (DdManager *table, int lower, int upper) |
| static int | zddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh) |
| static int | zddGroupSiftingUp (DdManager *table, int y, int xLow, Move **moves) |
| static int | zddGroupSiftingDown (DdManager *table, int x, int xHigh, Move **moves) |
| static int | zddGroupMove (DdManager *table, int x, int y, Move **moves) |
| static int | zddGroupMoveBackward (DdManager *table, int x, int y) |
| static int | zddGroupSiftingBackward (DdManager *table, Move *moves, int size) |
| static void | zddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high) |
| int | cuddZddTreeSifting (DdManager *table, Cudd_ReorderingType method) |
| DdNode * | cuddZddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I) |
| DdNode * | cuddBddIsop (DdManager *dd, DdNode *L, DdNode *U) |
| DdNode * | cuddMakeBddFromZddCover (DdManager *dd, DdNode *node) |
| static int | cuddZddLinearInPlace (DdManager *table, int x, int y) |
| static int | cuddZddLinearAux (DdManager *table, int x, int xLow, int xHigh) |
| static Move * | cuddZddLinearUp (DdManager *table, int y, int xLow, Move *prevMoves) |
| static Move * | cuddZddLinearDown (DdManager *table, int x, int xHigh, Move *prevMoves) |
| static int | cuddZddLinearBackward (DdManager *table, int size, Move *moves) |
| static Move * | cuddZddUndoMoves (DdManager *table, Move *moves) |
| int | cuddZddLinearSifting (DdManager *table, int lower, int upper) |
| static Move * | zddSwapAny (DdManager *table, int x, int y) |
| static int | cuddZddSiftingAux (DdManager *table, int x, int x_low, int x_high) |
| static Move * | cuddZddSiftingUp (DdManager *table, int x, int x_low, int initial_size) |
| static Move * | cuddZddSiftingDown (DdManager *table, int x, int x_high, int initial_size) |
| static int | cuddZddSiftingBackward (DdManager *table, Move *moves, int size) |
| static void | zddReorderPreprocess (DdManager *table) |
| static int | zddReorderPostprocess (DdManager *table) |
| static int | zddShuffle (DdManager *table, int *permutation) |
| static int | zddSiftUp (DdManager *table, int x, int xLow) |
| static void | zddFixTree (DdManager *table, MtrNode *treenode) |
| int | Cudd_zddReduceHeap (DdManager *table, Cudd_ReorderingType heuristic, int minsize) |
| int | cuddZddAlignToBdd (DdManager *table) |
| int | cuddZddNextHigh (DdManager *table, int x) |
| int | cuddZddNextLow (DdManager *table, int x) |
| int | cuddZddUniqueCompare (int *ptr_x, int *ptr_y) |
| int | cuddZddSwapInPlace (DdManager *table, int x, int y) |
| int | cuddZddSwapping (DdManager *table, int lower, int upper, Cudd_ReorderingType heuristic) |
| int | cuddZddSifting (DdManager *table, int lower, int upper) |
| static DdNode * | zdd_subset1_aux (DdManager *zdd, DdNode *P, DdNode *zvar) |
| static DdNode * | zdd_subset0_aux (DdManager *zdd, DdNode *P, DdNode *zvar) |
| static void | zddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty) |
| DdNode * | Cudd_zddDiffConst (DdManager *zdd, DdNode *P, DdNode *Q) |
| DdNode * | cuddZddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h) |
| DdNode * | cuddZddUnion (DdManager *zdd, DdNode *P, DdNode *Q) |
| DdNode * | cuddZddIntersect (DdManager *zdd, DdNode *P, DdNode *Q) |
| DdNode * | cuddZddDiff (DdManager *zdd, DdNode *P, DdNode *Q) |
| DdNode * | cuddZddChangeAux (DdManager *zdd, DdNode *P, DdNode *zvar) |
| DdNode * | cuddZddSubset1 (DdManager *dd, DdNode *P, int var) |
| DdNode * | cuddZddSubset0 (DdManager *dd, DdNode *P, int var) |
| static int | cuddZddSymmSiftingAux (DdManager *table, int x, int x_low, int x_high) |
| static int | cuddZddSymmSiftingConvAux (DdManager *table, int x, int x_low, int x_high) |
| static Move * | cuddZddSymmSifting_up (DdManager *table, int x, int x_low, int initial_size) |
| static Move * | cuddZddSymmSifting_down (DdManager *table, int x, int x_high, int initial_size) |
| static int | cuddZddSymmSiftingBackward (DdManager *table, Move *moves, int size) |
| static int | zdd_group_move (DdManager *table, int x, int y, Move **moves) |
| static int | zdd_group_move_backward (DdManager *table, int x, int y) |
| static void | cuddZddSymmSummary (DdManager *table, int lower, int upper, int *symvars, int *symgroups) |
| int | cuddZddSymmCheck (DdManager *table, int x, int y) |
| int | cuddZddSymmSifting (DdManager *table, int lower, int upper) |
| int | cuddZddSymmSiftingConv (DdManager *table, int lower, int upper) |
Variables | |
| static char rcsid [] | DD_UNUSED = "$Id: cuddAddIte.c,v 1.16 2012/02/05 01:07:18 fabio Exp $" |
| static int | popsize |
| static int | numvars |
| static int * | storedd |
| static st_table * | computed |
| static int * | repeat |
| static int | large |
| static int | result |
| static int | cross |
| static int * | entry |
| int | ddTotalNumberSwapping |
| static unsigned int | originalSize |
| static DdNode * | one |
| static DdNode * | zero |
| static DdNode * | background |
| static long | cuddRand = 0 |
| static long | cuddRand2 |
| static long | shuffleSelect |
| static long | shuffleTable [STAB_SIZE] |
| int | zddTotalNumberSwapping |
| int * | zdd_entry |
| static int | zddTotalNumberLinearTr |
| static DdNode * | empty |
| #define ABC 1 |
| #define ABCD 1 |
| #define ABDC 8 |
| #define ACB 6 |
| #define ACBD 2 |
| #define ACDB 4 |
| #define ADBC 14 |
| #define ADCB 9 |
| #define BAC 2 |
| #define BACD 7 |
| #define BADC 13 |
| #define bang | ( | f | ) | ((Cudd_IsComplement(f)) ? '!' : ' ') |
| #define BCA 3 |
| #define BCAD 10 |
| #define BCDA 16 |
| #define BDAC 19 |
| #define BDCA 21 |
| #define BETA 0.6 |
CFile***********************************************************************
FileName [cuddAnneal.c]
PackageName [cudd]
Synopsis [Reordering of DDs based on simulated annealing]
Description [Internal procedures included in this file:
Static procedures included in this file:
]
SeeAlso []
Author [Jae-Young Jang, Jorgen Sivesind]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define BPL 32 |
CFile***********************************************************************
FileName [cuddInteract.c]
PackageName [cudd]
Synopsis [Functions to manipulate the variable interaction matrix.]
Description [Internal procedures included in this file:
Static procedures included in this file:
The interaction matrix tells whether two variables are both in the support of some function of the DD. The main use of the interaction matrix is in the in-place swapping. Indeed, if two variables do not interact, there is no arc connecting the two layers; therefore, the swap can be performed in constant time, without scanning the subtables. Another use of the interaction matrix is in the computation of the lower bounds for sifting. Finally, the interaction matrix can be used to speed up aggregation checks in symmetric and group sifting.
The computation of the interaction matrix is done with a series of depth-first searches. The searches start from those nodes that have only external references. The matrix is stored as a packed array of bits; since it is symmetric, only the upper triangle is kept in memory. As a final remark, we note that there may be variables that do interact, but that for a given variable order have no arc connecting their layers when they are adjacent. For instance, in ite(a,b,c) with the order a<b<c, b and c interact, but are not connected.]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define BPL 32 |
CFile***********************************************************************
FileName [cuddInteract.c]
PackageName [cudd]
Synopsis [Functions to manipulate the variable interaction matrix.]
Description [Internal procedures included in this file:
Static procedures included in this file:
The interaction matrix tells whether two variables are both in the support of some function of the DD. The main use of the interaction matrix is in the in-place swapping. Indeed, if two variables do not interact, there is no arc connecting the two layers; therefore, the swap can be performed in constant time, without scanning the subtables. Another use of the interaction matrix is in the computation of the lower bounds for sifting. Finally, the interaction matrix can be used to speed up aggregation checks in symmetric and group sifting.
The computation of the interaction matrix is done with a series of depth-first searches. The searches start from those nodes that have only external references. The matrix is stored as a packed array of bits; since it is symmetric, only the upper triangle is kept in memory. As a final remark, we note that there may be variables that do interact, but that for a given variable order have no arc connecting their layers when they are adjacent. For instance, in ite(a,b,c) with the order a<b<c, b and c interact, but are not connected.]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define CAB 5 |
| #define CABD 3 |
| #define CADB 6 |
| #define CBA 4 |
| #define CBAD 5 |
| #define CBDA 11 |
| #define CDAB 12 |
| #define CDBA 17 |
| #define CUDD_SWAP_MOVE 0 |
CFile***********************************************************************
FileName [cuddLinear.c]
PackageName [cudd]
Synopsis [Functions for DD reduction by linear transformations.]
Description [ Internal procedures included in this module:
Static procedures included in this module:
]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
CFile***********************************************************************
FileName [cuddZddLin.c]
PackageName [cudd]
Synopsis [Procedures for dynamic variable ordering of ZDDs.]
Description [Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso [cuddLinear.c cuddZddReord.c]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define CUDD_SWAP_MOVE 0 |
CFile***********************************************************************
FileName [cuddLinear.c]
PackageName [cudd]
Synopsis [Functions for DD reduction by linear transformations.]
Description [ Internal procedures included in this module:
Static procedures included in this module:
]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
CFile***********************************************************************
FileName [cuddZddLin.c]
PackageName [cudd]
Synopsis [Procedures for dynamic variable ordering of ZDDs.]
Description [Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso [cuddLinear.c cuddZddReord.c]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define DABC 20 |
| #define DACB 15 |
| #define DBAC 23 |
| #define DBCA 24 |
| #define DCAB 18 |
| #define DCBA 22 |
| #define DD_BIGGY 100000000 |
CFile***********************************************************************
FileName [cuddSat.c]
PackageName [cudd]
Synopsis [Functions for the solution of satisfiability related problems.]
Description [External procedures included in this file:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Seh-Woong Jeong, Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define DD_MAX_HASHTABLE_DENSITY 2 /* tells when to resize a table */ |
CFile***********************************************************************
FileName [cuddLCache.c]
PackageName [cudd]
Synopsis [Functions for local caches.]
Description [Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define DD_MAX_SUBTABLE_SPARSITY 8 |
CFile***********************************************************************
FileName [cuddReorder.c]
PackageName [cudd]
Synopsis [Functions for dynamic variable reordering.]
Description [External procedures included in this file:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Shipra Panda, Bernard Plessier, Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
CFile***********************************************************************
FileName [cuddZddReord.c]
PackageName [cudd]
Synopsis [Procedures for dynamic variable ordering of ZDDs.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Hyong-Kyoon Shin, In-Ho Moon]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define DD_MAX_SUBTABLE_SPARSITY 8 |
CFile***********************************************************************
FileName [cuddReorder.c]
PackageName [cudd]
Synopsis [Functions for dynamic variable reordering.]
Description [External procedures included in this file:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Shipra Panda, Bernard Plessier, Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
CFile***********************************************************************
FileName [cuddZddReord.c]
PackageName [cudd]
Synopsis [Procedures for dynamic variable ordering of ZDDs.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Hyong-Kyoon Shin, In-Ho Moon]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define DD_NORMAL_SIFT 0 |
CFile***********************************************************************
FileName [cuddGroup.c]
PackageName [cudd]
Synopsis [Functions for group sifting.]
Description [External procedures included in this file:
Internal procedures included in this file:
Static procedures included in this module:
]
Author [Shipra Panda, Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define ddLCHash1 | ( | f, | |
| shift | |||
| ) | (((unsigned)(f) * DD_P1) >> (shift)) |
| #define ddLCHash3 | ( | f, | |
| g, | |||
| h, | |||
| shift | |||
| ) | ddCHash2(f,g,h,shift) |
| #define MODULUS1 2147483563 |
CFile***********************************************************************
FileName [cuddUtil.c]
PackageName [cudd]
Synopsis [Utility functions.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define MV_OOM (Move *)1 |
CFile***********************************************************************
FileName [cuddSymmetry.c]
PackageName [cudd]
Synopsis [Functions for symmetry-based variable reordering.]
Description [External procedures included in this file:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Shipra Panda, Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| #define WEIGHT | ( | weight, | |
| col | |||
| ) | ((weight) == NULL ? 1 : weight[col]) |
| #define ZDD_MV_OOM (Move *)1 |
CFile***********************************************************************
FileName [cuddZddSymm.c]
PackageName [cudd]
Synopsis [Functions for symmetry-based ZDD variable reordering.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso [cuddSymmetry.c]
Author [Hyong-Kyoon Shin, In-Ho Moon]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
| typedef struct cuddPathPair cuddPathPair |
CFile***********************************************************************
FileName [cuddTable.c]
PackageName [cudd]
Synopsis [Unique table management functions.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
|
static |
Function********************************************************************
Synopsis [Adds multiplicity groups to a ZDD variable group tree.]
Description [Adds multiplicity groups to a ZDD variable group tree. Returns 1 if successful; 0 otherwise. This function creates the groups for set of ZDD variables (whose cardinality is given by parameter multiplicity) that are created for each BDD variable in Cudd_zddVarsFromBddVars. The crux of the matter is to determine the index each new group. (The index of the first variable in the group.) We first build all the groups for the children of a node, and then deal with the ZDD variables that are directly attached to the node. The problem for these is that the tree itself does not provide information on their position inside the group. While we deal with the children of the node, therefore, we keep track of all the positions they occupy. The remaining positions in the tree can be freely used. Also, we keep track of all the variables placed in the children. All the remaining variables are directly attached to the group. We can then place any pair of variables not yet grouped in any pair of available positions in the node.]
SideEffects [Changes the variable group tree.]
SeeAlso [Cudd_zddVarsFromBddVars]
Definition at line 2169 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Replaces variables with constants if possible (part of canonical form).]
Description []
SideEffects [None]
Definition at line 590 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Comparison function for the computed table.]
Description [Comparison function for the computed table. Returns 0 if the two arrays are equal; 1 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 8050 of file cuddInt.c.
|
static |
CFile***********************************************************************
FileName [cuddBddAbs.c]
PackageName [cudd]
Synopsis [Quantification functions for BDDs.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart
Function********************************************************************
Synopsis [Checks whether cube is an BDD representing the product of positive literals.]
Description [Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 2791 of file cuddInt.c.
Function********************************************************************
Synopsis [Fixes the BDD variable group tree after a shuffle.]
Description [Fixes the BDD variable group tree after a shuffle. Assumes that the order of the variables in a terminal node has not been changed.]
SideEffects [Changes the BDD variable group tree.]
SeeAlso []
Definition at line 16331 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Picks unique member from equiv expressions.]
Description [Reduces 2 variable expressions to canonical form.]
SideEffects [None]
SeeAlso [bddVarToConst bddVarToCanonicalSimple]
Definition at line 3917 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Picks unique member from equiv expressions.]
Description [Makes sure the first two pointers are regular. This mat require the complementation of the result, which is signaled by returning 1 instead of 0. This function is simpler than the general case because it assumes that no two arguments are the same or complementary, and no argument is constant.]
SideEffects [None]
SeeAlso [bddVarToConst bddVarToCanonical]
Definition at line 4019 of file cuddInt.c.
CFile***********************************************************************
FileName [cuddBddIte.c]
PackageName [cudd]
Synopsis [BDD ITE function and satellites.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart
Function********************************************************************
Synopsis [Replaces variables with constants if possible.]
Description [This function performs part of the transformation to standard form by replacing variables with constants if possible.]
SideEffects [None]
SeeAlso [bddVarToCanonical bddVarToCanonicalSimple]
Definition at line 3882 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Builds a DD from a given order.]
Description [Builds a DD from a given order. This procedure also sifts the final order and inserts into the array the size in nodes of the result. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 7897 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Check symmetry condition.]
Description [Returns 1 if a variable is the one with the highest index among those belonging to a symmetry group that are in the top part of the BDD. The top part is given by level.]
SideEffects [None]
SeeAlso [initSymmInfo]
|
static |
Function********************************************************************
Synopsis [Computes a lower bound on the size of a BDD.]
Description [Computes a lower bound on the size of a BDD from the following factors:
variable in the support of the roots in the upper part of the BDD subjected to reordering.
SideEffects [None]
SeeAlso []
Definition at line 7134 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Copies the current variable order to array.]
Description [Copies the current variable order to array. At the same time inverts the permutation.]
SideEffects [None]
SeeAlso []
Definition at line 1365 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the complement of an ADD a la C language.]
Description [Computes the complement of an ADD a la C language: The complement of 0 is 1 and the complement of everything else is 0. Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addNegate]
Definition at line 312 of file cuddInt.c.
Function********************************************************************
Synopsis [Checks whether ADD g is constant whenever ADD f is 1.]
Description [Checks whether ADD g is constant whenever ADD f is 1. f must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may or may not be constant) or DD_NON_CONSTANT. If f is identically 0, the check is assumed to be successful, and the background value is returned. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_addIteConstant Cudd_addLeq]
Definition at line 225 of file cuddInt.c.
AutomaticEnd Function********************************************************************
Synopsis [Implements ITEconstant for ADDs.]
Description [Implements ITEconstant for ADDs. f must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may or may not be constant) or DD_NON_CONSTANT. No new nodes are created. This function can be used, for instance, to check that g has a constant value (specified by h) whenever f is 1. If the constant value is unknown, then one should use Cudd_addEvalConst.]
SideEffects [None]
SeeAlso [Cudd_addIte Cudd_addEvalConst Cudd_bddIteConstant]
Definition at line 128 of file cuddInt.c.
Function********************************************************************
Synopsis [Determines whether f is less than or equal to g.]
Description [Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created. This procedure works for arbitrary ADDs. For 0-1 ADDs Cudd_addEvalConst is more efficient.]
SideEffects [None]
SeeAlso [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]
Definition at line 341 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the conjunction of two BDDs f and g.]
Description [Computes the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAndAbstract Cudd_bddIntersect Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
Definition at line 3114 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the conjunction of two BDDs f and g. Returns NULL if too many nodes are required.]
Description [Computes the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up or more new nodes than limit are required.]
SideEffects [None]
SeeAlso [Cudd_bddAnd]
Definition at line 3146 of file cuddInt.c.
AutomaticEnd Function********************************************************************
Synopsis [Existentially abstracts all the variables in cube from f.]
Description [Existentially abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddUnivAbstract Cudd_addExistAbstract]
Definition at line 2331 of file cuddInt.c.
Function********************************************************************
Synopsis [Returns a function included in the intersection of f and g.]
Description [Computes a function included in the intersection of f and g. (That is, a witness that the intersection is not empty.) Cudd_bddIntersect tries to build as few new nodes as possible. If the only result of interest is whether f and g intersect, Cudd_bddLeq should be used instead.]
SideEffects [None]
SeeAlso [Cudd_bddLeq Cudd_bddIteConstant]
Definition at line 3082 of file cuddInt.c.
| int Cudd_bddIsVarToBeGrouped | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is set to be grouped.]
Description [Checks whether a variable is set to be grouped. This function is used for lazy sifting.]
SideEffects [none]
SeeAlso []
Definition at line 2067 of file cuddInt.c.
| int Cudd_bddIsVarToBeUngrouped | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Checks whether a variable is set to be ungrouped.]
Description [Checks whether a variable is set to be ungrouped. This function is used for lazy sifting. Returns 1 if the variable is marked to be ungrouped; 0 if the variable exists, but it is not marked to be ungrouped; -1 if the variable does not exist.]
SideEffects [none]
SeeAlso [Cudd_bddSetVarToBeUngrouped]
Definition at line 2096 of file cuddInt.c.
AutomaticEnd Function********************************************************************
Synopsis [Implements ITE(f,g,h).]
Description [Implements ITE(f,g,h). Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_addIte Cudd_bddIteConstant Cudd_bddIntersect]
Definition at line 2942 of file cuddInt.c.
Function********************************************************************
Synopsis [Implements ITEconstant(f,g,h).]
Description [Implements ITEconstant(f,g,h). Returns a pointer to the resulting BDD (which may or may not be constant) or DD_NON_CONSTANT. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant]
Definition at line 2974 of file cuddInt.c.
AutomaticEnd Function********************************************************************
Synopsis [Returns the BDD variable with index i.]
Description [Retrieves the BDD variable with index i if it already exists, or creates a new BDD variable. Returns a pointer to the variable if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddNewVar Cudd_addIthVar Cudd_bddNewVarAtLevel Cudd_ReadVars]
Definition at line 1685 of file cuddInt.c.
Function********************************************************************
Synopsis [Determines whether f is less than or equal to g.]
Description [Returns 1 if f is less than or equal to g; 0 otherwise. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_bddIteConstant Cudd_addEvalConst]
Definition at line 3283 of file cuddInt.c.
Function********************************************************************
Synopsis [Tells whether f is less than of equal to G unless D is 1.]
Description [Tells whether f is less than of equal to G unless D is
SideEffects [None]
SeeAlso [Cudd_EquivDC Cudd_bddLeq Cudd_bddIteConstant]
Definition at line 16870 of file cuddInt.c.
Function********************************************************************
Synopsis [Expands cube to a prime implicant of f.]
Description [Expands cube to a prime implicant of f. Returns the prime if successful; NULL otherwise. In particular, NULL is returned if cube is not a real cube or is not an implicant of f.]
SideEffects [None]
SeeAlso [Cudd_bddMaximallyExpand]
Definition at line 17112 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the disjunction of two BDDs f and g.]
Description [Computes the disjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor Cudd_bddXor Cudd_bddXnor]
Definition at line 3181 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the disjunction of two BDDs f and g. Returns NULL if too many nodes are required.]
Description [Computes the disjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up or more new nodes than limit are required.]
SideEffects [None]
SeeAlso [Cudd_bddOr]
Definition at line 3214 of file cuddInt.c.
| int Cudd_bddReadPairIndex | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Reads a corresponding pair index for a given index.]
Description [Reads a corresponding pair index for a given index. These pair indices are present and next state variable. Returns the corresponding variable index if the variable exists; -1 otherwise.]
SideEffects [modifies the manager]
SeeAlso [Cudd_bddSetPairIndex]
Definition at line 2044 of file cuddInt.c.
Function********************************************************************
Synopsis [Builds a positional array from the BDD of a cube.]
Description [Builds a positional array from the BDD of a cube. Array must have one entry for each BDD variable. The positional array has 1 in i-th position if the variable of index i appears in true form in the cube; it has 0 in i-th position if the variable of index i appears in complemented form in the cube; finally, it has 2 in i-th position if the variable of index i does not appear in the cube. Returns 1 if successful (the BDD is indeed a cube); 0 otherwise.]
SideEffects [The result is in the array passed by reference.]
SeeAlso [Cudd_CubeArrayToBdd]
Definition at line 22669 of file cuddInt.c.
Function********************************************************************
Synopsis [Checks whether a variable is dependent on others in a function.]
Description [Checks whether a variable is dependent on others in a function. Returns 1 if the variable is dependent; 0 otherwise. No new nodes are created.]
SideEffects [None]
SeeAlso []
Definition at line 2369 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the exclusive OR of two BDDs f and g.]
Description [Computes the exclusive OR of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]
SideEffects [None]
SeeAlso [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNand Cudd_bddNor Cudd_bddXnor]
Definition at line 3253 of file cuddInt.c.
Function********************************************************************
Synopsis [Checks whether g is the BDD of a cube.]
Description [Checks whether g is the BDD of a cube. Returns 1 in case of success; 0 otherwise. The constant 1 is a valid cube, but all other constant functions cause cuddCheckCube to return 0.]
SideEffects [None]
SeeAlso []
Definition at line 6155 of file cuddInt.c.
| int Cudd_CheckKeys | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Checks for several conditions that should not occur.]
Description [Checks for the following conditions:
Reports the average length of non-empty lists. Returns the number of subtables for which the number of keys is wrong.]
SideEffects [None]
SeeAlso [Cudd_DebugCheck]
Definition at line 5577 of file cuddInt.c.
CFile***********************************************************************
FileName [cuddCof.c]
PackageName [cudd]
Synopsis [Cofactoring functions.]
Description [External procedures included in this module:
Internal procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Computes the cofactor of f with respect to g.]
Description [Computes the cofactor of f with respect to g; g must be the BDD or the ADD of a cube. Returns a pointer to the cofactor if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddConstrain Cudd_bddRestrict]
Definition at line 6119 of file cuddInt.c.
AutomaticEnd Function********************************************************************
Synopsis [Counts the number of minterms of a DD.]
Description [Counts the number of minterms of a DD. The function is assumed to depend on nvars variables. The minterm count is represented as a double, to allow for a larger number of variables. Returns the number of minterms of the function rooted at node if successful; (double) CUDD_OUT_OF_MEM otherwise.]
SideEffects [None]
SeeAlso [Cudd_PrintDebug Cudd_CountPath]
Definition at line 22209 of file cuddInt.c.
| int Cudd_DebugCheck | ( | DdManager * | table | ) |
AutomaticEnd Function********************************************************************
Synopsis [Checks for inconsistencies in the DD heap.]
Description [Checks for inconsistencies in the DD heap:
Returns 0 if no inconsistencies are found; DD_OUT_OF_MEM if there is not enough memory; 1 otherwise.]
SideEffects [None]
SeeAlso [Cudd_CheckKeys]
Definition at line 5255 of file cuddInt.c.
Function********************************************************************
Synopsis [Determines whether a BDD is negative unate in a variable.]
Description [Determines whether the function represented by BDD f is negative unate (monotonic decreasing) in variable i. Returns the constant one is f is unate and the (logical) constant zero if it is not. This function does not generate any new nodes.]
SideEffects [None]
SeeAlso [Cudd_Increasing]
Definition at line 16691 of file cuddInt.c.
| void Cudd_Deref | ( | DdNode * | node | ) |
Function********************************************************************
Synopsis [Decreases the reference count of node.]
Description [Decreases the reference count of node. It is primarily used in recursive procedures to decrease the ref count of a result node before returning it. This accomplishes the goal of removing the protection applied by a previous Cudd_Ref.]
SideEffects [None]
SeeAlso [Cudd_RecursiveDeref Cudd_RecursiveDerefZdd Cudd_Ref]
Definition at line 14198 of file cuddInt.c.
| int Cudd_EqualSupNorm | ( | DdManager * | dd, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| CUDD_VALUE_TYPE | tolerance, | ||
| int | pr | ||
| ) |
Function********************************************************************
Synopsis [Compares two ADDs for equality within tolerance.]
Description [Compares two ADDs for equality within tolerance. Two ADDs are reported to be equal if the maximum difference between them (the sup norm of their difference) is less than or equal to the tolerance parameter. Returns 1 if the two ADDs are equal (within tolerance); 0 otherwise. If parameter pr is positive the first failure is reported to the standard output.]
SideEffects [None]
SeeAlso []
Definition at line 17044 of file cuddInt.c.
Function********************************************************************
Synopsis [Tells whether F and G are identical wherever D is 0.]
Description [Tells whether F and G are identical wherever D is 0. F and G are either two ADDs or two BDDs. D is either a 0-1 ADD or a BDD. The function returns 1 if F and G are equivalent, and 0 otherwise. No new nodes are created.]
SideEffects [None]
SeeAlso [Cudd_bddLeqUnless]
Definition at line 16770 of file cuddInt.c.
| DdGen* Cudd_FirstCube | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int ** | cube, | ||
| CUDD_VALUE_TYPE * | value | ||
| ) |
Function********************************************************************
Synopsis [Finds the first cube of a decision diagram.]
Description [Defines an iterator on the onset of a decision diagram and finds its first cube. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.
A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a disjoint cover of the function associated with the diagram. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.
For each cube, a value is also returned. This value is always 1 for a BDD, while it may be different from 1 for an ADD. For BDDs, the offset is the set of cubes whose value is the logical zero. For ADDs, the offset is the set of cubes whose value is the background value. The cubes of the offset are not enumerated.]
SideEffects [The first cube and its value are returned as side effects.]
SeeAlso [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstNode]
Definition at line 22267 of file cuddInt.c.
Function********************************************************************
Synopsis [Finds the first node of a decision diagram.]
Description [Defines an iterator on the nodes of a decision diagram and finds its first node. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise. The nodes are enumerated in a reverse topological order, so that a node is always preceded in the enumeration by its descendants.]
SideEffects [The first node is returned as a side effect.]
SeeAlso [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube]
Function********************************************************************
Synopsis [Finds the first prime of a Boolean function.]
Description [Defines an iterator on a pair of BDDs describing a (possibly incompletely specified) Boolean functions and finds the first cube of a cover of the function. Returns a generator that contains the information necessary to continue the enumeration if successful; NULL otherwise.
The two argument BDDs are the lower and upper bounds of an interval. It is a mistake to call this function with a lower bound that is not less than or equal to the upper bound.
A cube is represented as an array of literals, which are integers in {0, 1, 2}; 0 represents a complemented literal, 1 represents an uncomplemented literal, and 2 stands for don't care. The enumeration produces a prime and irredundant cover of the function associated with the two BDDs. The size of the array equals the number of variables in the manager at the time Cudd_FirstCube is called.
This iterator can only be used on BDDs.]
SideEffects [The first cube is returned as side effect.]
SeeAlso [Cudd_ForeachPrime Cudd_NextPrime Cudd_GenFree Cudd_IsGenEmpty Cudd_FirstCube Cudd_FirstNode]
Definition at line 22497 of file cuddInt.c.
| void Cudd_FreeTree | ( | DdManager * | dd | ) |
| void Cudd_FreeZddTree | ( | DdManager * | dd | ) |
| int Cudd_GenFree | ( | DdGen * | gen | ) |
Function********************************************************************
Synopsis [Frees a CUDD generator.]
Description [Frees a CUDD generator. Always returns 0, so that it can be used in mis-like foreach constructs.]
SideEffects [None]
SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty]
Definition at line 22814 of file cuddInt.c.
| DdManager* Cudd_Init | ( | unsigned int | numVars, |
| unsigned int | numVarsZ, | ||
| unsigned int | numSlots, | ||
| unsigned int | cacheSize, | ||
| unsigned long | maxMemory | ||
| ) |
CFile***********************************************************************
FileName [cuddInit.c]
PackageName [cudd]
Synopsis [Functions to initialize and shut down the DD manager.]
Description [External procedures included in this module:
Internal procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Creates a new DD manager.]
Description [Creates a new DD manager, initializes the table, the basic constants and the projection functions. If maxMemory is 0, Cudd_Init decides suitable values for the maximum size of the cache and for the limit for fast unique table growth based on the available memory. Returns a pointer to the manager if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_Quit]
Definition at line 10544 of file cuddInt.c.
| int Cudd_IsGenEmpty | ( | DdGen * | gen | ) |
Function********************************************************************
Synopsis [Queries the status of a generator.]
Description [Queries the status of a generator. Returns 1 if the generator is empty or NULL; 0 otherswise.]
SideEffects [None]
SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube Cudd_FirstNode Cudd_NextNode Cudd_GenFree]
Definition at line 22854 of file cuddInt.c.
Function********************************************************************
Synopsis [Decreases the reference count of BDD node n.]
Description [Decreases the reference count of node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a BDD that is no longer needed. It is more efficient than Cudd_RecursiveDeref, but it cannot be used on ADDs. The greater efficiency comes from being able to assume that no constant node will ever die as a result of a call to this procedure.]
SideEffects [None]
SeeAlso [Cudd_RecursiveDeref Cudd_DelayedDerefBdd]
Definition at line 14090 of file cuddInt.c.
AutomaticEnd Function********************************************************************
Synopsis [Finds a largest cube in a DD.]
Description [Finds a largest cube in a DD. f is the DD we want to get the largest cube for. The problem is translated into the one of finding a shortest path in f, when both THEN and ELSE arcs are assumed to have unit length. This yields a largest cube in the disjoint cover corresponding to the DD. Therefore, it is not necessarily the largest implicant of f. Returns the largest cube as a BDD.]
SideEffects [The number of literals of the cube is returned in the location pointed by length if it is non-null.]
SeeAlso [Cudd_ShortestPath]
Definition at line 16616 of file cuddInt.c.
| int Cudd_NextCube | ( | DdGen * | gen, |
| int ** | cube, | ||
| CUDD_VALUE_TYPE * | value | ||
| ) |
Function********************************************************************
Synopsis [Generates the next cube of a decision diagram onset.]
Description [Generates the next cube of a decision diagram onset, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]
SideEffects [The cube and its value are returned as side effects. The generator is modified.]
SeeAlso [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty Cudd_NextNode]
Function********************************************************************
Synopsis [Finds the next node of a decision diagram.]
Description [Finds the node of a decision diagram, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]
SideEffects [The next node is returned as a side effect.]
SeeAlso [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube]
Definition at line 22782 of file cuddInt.c.
| int Cudd_NextPrime | ( | DdGen * | gen, |
| int ** | cube | ||
| ) |
Function********************************************************************
Synopsis [Generates the next prime of a Boolean function.]
Description [Generates the next cube of a Boolean function, using generator gen. Returns 0 if the enumeration is completed; 1 otherwise.]
SideEffects [The cube and is returned as side effects. The generator is modified.]
SeeAlso [Cudd_ForeachPrime Cudd_FirstPrime Cudd_GenFree Cudd_IsGenEmpty Cudd_NextCube Cudd_NextNode]
Definition at line 22599 of file cuddInt.c.
| void Cudd_OutOfMem | ( | long | size | ) |
Function********************************************************************
Synopsis [Warns that a memory allocation failed.]
Description [Warns that a memory allocation failed. This function can be used as replacement of MMout_of_memory to prevent the safe_mem functions of the util package from exiting when malloc returns NULL. One possible use is in case of discretionary allocations; for instance, the allocation of memory to enlarge the computed table.]
SideEffects [None]
SeeAlso []
| int Cudd_PrintLinear | ( | DdManager * | table | ) |
AutomaticEnd Function********************************************************************
Synopsis [Prints the linear transform matrix.]
Description [Prints the linear transform matrix. Returns 1 in case of success; 0 otherwise.]
SideEffects [none]
SeeAlso []
Definition at line 12695 of file cuddInt.c.
| void Cudd_Quit | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Deletes resources associated with a DD manager.]
Description [Deletes resources associated with a DD manager and resets the global statistical counters. (Otherwise, another manaqger subsequently created would inherit the stats of this one.)]
SideEffects [None]
SeeAlso [Cudd_Init]
Definition at line 10641 of file cuddInt.c.
| long Cudd_Random | ( | void | ) |
Function********************************************************************
Synopsis [Portable random number generator.]
Description [Portable number generator based on ran2 from "Numerical Recipes in C." It is a long period (> 2 * 10^18) random number generator of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly distributed between 0 and 2147483561 (inclusive of the endpoint values). The random generator can be explicitly initialized by calling Cudd_Srandom. If no explicit initialization is performed, then the seed 1 is assumed.]
SideEffects [None]
SeeAlso [Cudd_Srandom]
Definition at line 22881 of file cuddInt.c.
| CUDD_VALUE_TYPE Cudd_ReadEpsilon | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reads the epsilon parameter of the manager.]
Description [Reads the epsilon parameter of the manager. The epsilon parameter control the comparison between floating point numbers.]
SideEffects [None]
SeeAlso [Cudd_SetEpsilon]
Definition at line 1883 of file cuddInt.c.
Function********************************************************************
Synopsis [Returns the logic zero constant of the manager.]
Description [Returns the zero constant of the manager. The logic zero constant is the complement of the one constant, and is distinct from the arithmetic zero.]
SideEffects [None]
SeeAlso [Cudd_ReadOne Cudd_ReadZero]
Definition at line 1738 of file cuddInt.c.
| unsigned long Cudd_ReadMemoryInUse | ( | DdManager * | dd | ) |
| long Cudd_ReadNodeCount | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Reports the number of nodes in BDDs and ADDs.]
Description [Reports the number of live nodes in BDDs and ADDs. This number does not include the isolated projection functions and the unused constants. These nodes that are not counted are not part of the DDs manipulated by the application.]
SideEffects [None]
SeeAlso [Cudd_ReadPeakNodeCount Cudd_zddReadNodeCount]
Definition at line 1948 of file cuddInt.c.
Function********************************************************************
Synopsis [Returns the one constant of the manager.]
Description [Returns the one constant of the manager. The one constant is common to ADDs and BDDs.]
SideEffects [None]
SeeAlso [Cudd_ReadZero Cudd_ReadLogicZero Cudd_ReadZddOne]
Definition at line 1716 of file cuddInt.c.
| int Cudd_ReadPerm | ( | DdManager * | dd, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Returns the current position of the i-th variable in the order.]
Description [Returns the current position of the i-th variable in the order. If the index is CUDD_CONST_INDEX, returns CUDD_CONST_INDEX; otherwise, if the index is out of bounds returns -1.]
SideEffects [None]
SeeAlso [Cudd_ReadInvPerm Cudd_ReadPermZdd]
Definition at line 1859 of file cuddInt.c.
| int Cudd_ReadSize | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Decreases the reference count of node n.]
Description [Decreases the reference count of node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a DD that is no longer needed.]
SideEffects [None]
SeeAlso [Cudd_Deref Cudd_Ref Cudd_RecursiveDerefZdd]
Definition at line 14027 of file cuddInt.c.
Function********************************************************************
Synopsis [Decreases the reference count of ZDD node n.]
Description [Decreases the reference count of ZDD node n. If n dies, recursively decreases the reference counts of its children. It is used to dispose of a ZDD that is no longer needed.]
SideEffects [None]
SeeAlso [Cudd_Deref Cudd_Ref Cudd_RecursiveDeref]
Definition at line 14145 of file cuddInt.c.
| int Cudd_ReduceHeap | ( | DdManager * | table, |
| Cudd_ReorderingType | heuristic, | ||
| int | minsize | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Main dynamic reordering routine.]
Description [Main dynamic reordering routine. Calls one of the possible reordering procedures:
For sifting, symmetric sifting, group sifting, and window permutation it is possible to request reordering to convergence.
The core of all methods is the reordering procedure cuddSwapInPlace() which swaps two adjacent variables and is based on Rudell's paper. Returns 1 in case of success; 0 otherwise. In the case of symmetric sifting (with and without convergence) returns 1 plus the number of symmetric variables, in case of success.]
SideEffects [Changes the variable order for all diagrams and clears the cache.]
Definition at line 14558 of file cuddInt.c.
| void Cudd_Ref | ( | DdNode * | n | ) |
CFile***********************************************************************
FileName [cuddRef.c]
PackageName [cudd]
Synopsis [Functions that manipulate the reference counts.]
Description [External procedures included in this module:
Internal procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Increases the reference count of a node, if it is not saturated.]
Description []
SideEffects [None]
SeeAlso [Cudd_RecursiveDeref Cudd_Deref]
Definition at line 14002 of file cuddInt.c.
| int Cudd_RemoveHook | ( | DdManager * | dd, |
| DD_HFP | f, | ||
| Cudd_HookType | where | ||
| ) |
Function********************************************************************
Synopsis [Removes a function from a hook.]
Description [Removes a function from a hook. A hook is a list of application-provided functions called on certain occasions by the package. Returns 1 if successful; 0 the function was not in the list.]
SideEffects [None]
SeeAlso [Cudd_AddHook]
Definition at line 1991 of file cuddInt.c.
| void Cudd_SetEpsilon | ( | DdManager * | dd, |
| CUDD_VALUE_TYPE | ep | ||
| ) |
Function********************************************************************
Synopsis [Sets the epsilon parameter of the manager to ep.]
Description [Sets the epsilon parameter of the manager to ep. The epsilon parameter control the comparison between floating point numbers.]
SideEffects [None]
SeeAlso [Cudd_ReadEpsilon]
Definition at line 1904 of file cuddInt.c.
| void Cudd_SetMinHit | ( | DdManager * | dd, |
| unsigned int | hr | ||
| ) |
Function********************************************************************
Synopsis [Sets the hit rate that causes resizinig of the computed table.]
Description [Sets the minHit parameter of the manager. This parameter controls the resizing of the computed table. If the hit rate is larger than the specified value, and the cache is not already too large, then its size is doubled.]
SideEffects [None]
SeeAlso [Cudd_ReadMinHit]
Definition at line 1763 of file cuddInt.c.
| void Cudd_Srandom | ( | long | seed | ) |
Function********************************************************************
Synopsis [Initializer for the portable random number generator.]
Description [Initializer for the portable number generator based on ran2 in "Numerical Recipes in C." The input is the seed for the generator. If it is negative, its absolute value is taken as seed. If it is 0, then 1 is taken as seed. The initialized sets up the two recurrences used to generate a long-period stream, and sets up the shuffle table.]
SideEffects [None]
SeeAlso [Cudd_Random]
Definition at line 22943 of file cuddInt.c.
AutomaticEnd Function********************************************************************
Synopsis [Performs the inclusion test for ZDDs (P implies Q).]
Description [Inclusion test for ZDDs (P implies Q). No new nodes are generated by this procedure. Returns empty if true; a valid pointer different from empty or DD_NON_CONSTANT otherwise.]
SideEffects [None]
SeeAlso [Cudd_zddDiff]
Definition at line 31212 of file cuddInt.c.
| int Cudd_zddReduceHeap | ( | DdManager * | table, |
| Cudd_ReorderingType | heuristic, | ||
| int | minsize | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Main dynamic reordering routine for ZDDs.]
Description [Main dynamic reordering routine for ZDDs. Calls one of the possible reordering procedures:
For sifting and symmetric sifting it is possible to request reordering to convergence.
The core of all methods is the reordering procedure cuddZddSwapInPlace() which swaps two adjacent variables. Returns 1 in case of success; 0 otherwise. In the case of symmetric sifting (with and without convergence) returns 1 plus the number of symmetric variables, in case of success.]
SideEffects [Changes the variable order for all ZDDs and clears the cache.]
Definition at line 29608 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_addCmpl.]
Description [Performs the recursive step of Cudd_addCmpl. Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addCmpl]
Definition at line 527 of file cuddInt.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_addIte(f,g,h).]
Description [Implements the recursive step of Cudd_addIte(f,g,h). Returns a pointer to the resulting ADD if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_addIte]
Definition at line 410 of file cuddInt.c.
AutomaticEnd Function********************************************************************
Synopsis [Fast storage allocation for DdNodes in the table.]
Description [Fast storage allocation for DdNodes in the table. The first 4 bytes of a chunk contain a pointer to the next block; the rest contains DD_MEM_CHUNK spaces for DdNodes. Returns a pointer to a new node if successful; NULL is memory is full.]
SideEffects [None]
SeeAlso [cuddDynamicAllocNode]
Definition at line 19624 of file cuddInt.c.
| int cuddAnnealing | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Get new variable-order by simulated annealing algorithm.]
Description [Get x, y by random selection. Choose either exchange or jump randomly. In case of jump, choose between jump_up and jump_down randomly. Do exchange or jump and get optimal case. Loop until there is no improvement or temperature reaches minimum. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 761 of file cuddInt.c.
| int cuddBddAlignToZdd | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Reorders BDD variables according to the order of the ZDD variables.]
Description [Reorders BDD variables according to the order of the ZDD variables. This function can be called at the end of ZDD reordering to insure that the order of the BDD variables is consistent with the order of the ZDD variables. The number of ZDD variables must be a multiple of the number of BDD variables. Let M be the ratio of the two numbers. cuddBddAlignToZdd then considers the ZDD variables from M*i to (M+1)*i-1 as corresponding to BDD variable i. This function should be normally called from Cudd_zddReduceHeap, which clears the cache. Returns 1 in case of success; 0 otherwise.]
SideEffects [Changes the BDD variable order for all diagrams and performs garbage collection of the BDD unique table.]
SeeAlso [Cudd_ShuffleHeap Cudd_zddReduceHeap]
Definition at line 15572 of file cuddInt.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddAnd.]
Description [Implements the recursive step of Cudd_bddAnd by taking the conjunction of two BDDs. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddAnd]
Definition at line 3633 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive steps of Cudd_bddBoleanDiff.]
Description [Performs the recursive steps of Cudd_bddBoleanDiff. Returns the BDD obtained by XORing the cofactors of f with respect to var if successful; NULL otherwise. Exploits the fact that dF/dx = dF'/dx.]
SideEffects [None]
SeeAlso []
Definition at line 2719 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive steps of Cudd_bddExistAbstract.]
Description [Performs the recursive steps of Cudd_bddExistAbstract. Returns the BDD obtained by abstracting the variables of cube from f if successful; NULL otherwise. It is also used by Cudd_bddUnivAbstract.]
SideEffects [None]
SeeAlso [Cudd_bddExistAbstract Cudd_bddUnivAbstract]
Definition at line 2437 of file cuddInt.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddIntersect.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIntersect]
Definition at line 3518 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_bddIsop]
Definition at line 28135 of file cuddInt.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddIte.]
Description [Implements the recursive step of Cudd_bddIte. Returns a pointer to the resulting BDD. NULL if the intermediate result blows up or if reordering occurs.]
SideEffects [None]
SeeAlso []
Definition at line 3380 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddMakePrime.]
Description [Performs the recursive step of Cudd_bddMakePrime. Returns the prime if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 17148 of file cuddInt.c.
Function********************************************************************
Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.]
Description [Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddAndAbstract]
Definition at line 2547 of file cuddInt.c.
Function********************************************************************
Synopsis [Implements the recursive step of Cudd_bddXor.]
Description [Implements the recursive step of Cudd_bddXor by taking the exclusive OR of two BDDs. Returns a pointer to the result is successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddXor]
Definition at line 3761 of file cuddInt.c.
| void cuddCacheFlush | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Flushes the cache.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 5070 of file cuddInt.c.
| void cuddCacheInsert | ( | DdManager * | table, |
| ptruint | op, | ||
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | h, | ||
| DdNode * | data | ||
| ) |
Function********************************************************************
Synopsis [Inserts a result in the cache for a function with three operands.]
Description [Inserts a result in the cache for a function with three operands. The operator tag (see CUDD/cuddInt.h for details) is split and stored into unused bits of the first two pointers.]
SideEffects [None]
SeeAlso [cuddCacheInsert2 cuddCacheInsert1]
Definition at line 4283 of file cuddInt.c.
Function********************************************************************
Synopsis [Inserts a result in the cache for a function with two operands.]
Description []
SideEffects [None]
SeeAlso [cuddCacheInsert cuddCacheInsert2]
Definition at line 4371 of file cuddInt.c.
Function********************************************************************
Synopsis [Inserts a result in the cache for a function with two operands.]
Description []
SideEffects [None]
SeeAlso [cuddCacheInsert cuddCacheInsert1]
Definition at line 4329 of file cuddInt.c.
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f, g, and h.]
Description [Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso [cuddCacheLookup2 cuddCacheLookup1]
Definition at line 4413 of file cuddInt.c.
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f.]
Description [Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso [cuddCacheLookup cuddCacheLookup2]
Definition at line 4591 of file cuddInt.c.
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f.]
Description [Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso [cuddCacheLookupZdd cuddCacheLookup2Zdd]
Definition at line 4699 of file cuddInt.c.
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f and g.]
Description [Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso [cuddCacheLookup cuddCacheLookup1]
Definition at line 4537 of file cuddInt.c.
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f and g.]
Description [Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso [cuddCacheLookupZdd cuddCacheLookup1Zdd]
Definition at line 4645 of file cuddInt.c.
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f, g, and h.]
Description [Returns the result if found; it returns NULL if no result is found.]
SideEffects [None]
SeeAlso [cuddCacheLookup2Zdd cuddCacheLookup1Zdd]
Definition at line 4475 of file cuddInt.c.
| int cuddCacheProfile | ( | DdManager * | table, |
| FILE * | fp | ||
| ) |
Function********************************************************************
Synopsis [Computes and prints a profile of the cache usage.]
Description [Computes and prints a profile of the cache usage. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 4815 of file cuddInt.c.
| void cuddCacheResize | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Resizes the cache.]
Description []
SideEffects [None]
SeeAlso []
| void cuddClearDeathRow | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_Cofactor.]
Description [Performs the recursive step of Cudd_Cofactor. Returns a pointer to the cofactor if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_Cofactor]
Definition at line 6226 of file cuddInt.c.
Function********************************************************************
Synopsis [Recursively collects all the nodes of a DD in a symbol table.]
Description [Traverses the DD f and collects all its nodes in a symbol table. f is assumed to be a regular pointer and cuddCollectNodes guarantees this assumption in the recursive calls. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 23013 of file cuddInt.c.
| int cuddComputeFloorLog2 | ( | unsigned int | value | ) |
Function********************************************************************
Synopsis [Returns the floor of the logarithm to the base 2.]
Description [Returns the floor of the logarithm to the base 2. The input value is assumed to be greater than 0.]
SideEffects [None]
SeeAlso []
Definition at line 5102 of file cuddInt.c.
Function********************************************************************
Synopsis [Looks up in the cache for the result of op applied to f, g, and h.]
Description [Looks up in the cache for the result of op applied to f, g, and h. Assumes that the calling procedure (e.g., Cudd_bddIteConstant) is only interested in whether the result is constant or not. Returns the result if found (possibly DD_NON_CONSTANT); otherwise it returns NULL.]
SideEffects [None]
SeeAlso [cuddCacheLookup]
Definition at line 4756 of file cuddInt.c.
Function********************************************************************
Synopsis [Dynamically allocates a Node.]
Description [Dynamically allocates a Node. This procedure is similar to cuddAllocNode in Cudd_Table.c, but it does not attempt garbage collection, because during reordering there are no dead nodes. Returns a pointer to a new node if successful; NULL is memory is full.]
SideEffects [None]
SeeAlso [cuddAllocNode]
Definition at line 14727 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_CofactorEstimate.]
Description [Performs the recursive step of Cudd_CofactorEstimate. Returns an estimate of the number of nodes in the DD of a cofactor of node. Uses the least significant bit of the next field as visited flag. node is supposed to be regular; the invariant is maintained by this procedure.]
SideEffects [None]
SeeAlso []
Definition at line 23328 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_CofactorEstimateSimple.]
Description [Performs the recursive step of Cudd_CofactorEstimateSimple. Returns an estimate of the number of nodes in the DD of the positive cofactor of node. Uses the least significant bit of the next field as visited flag. node is supposed to be regular; the invariant is maintained by this procedure.]
SideEffects [None]
SeeAlso []
Definition at line 23487 of file cuddInt.c.
| int cuddExact | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Exact variable ordering algorithm.]
Description [Exact variable ordering algorithm. Finds an optimum order for the variables between lower and upper. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 6474 of file cuddInt.c.
| void cuddFreeTable | ( | DdManager * | unique | ) |
Function********************************************************************
Synopsis [Frees the resources associated to a unique table.]
Description []
SideEffects [None]
SeeAlso [cuddInitTable]
Definition at line 20050 of file cuddInt.c.
| int cuddGa | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Genetic algorithm for DD reordering.]
Description [Genetic algorithm for DD reordering. The two children of a crossover will be stored in storedd[popsize] and storedd[popsize+1] — the last two slots in the storedd array. (This will make comparisons and replacement easy.) Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 7533 of file cuddInt.c.
| int cuddGarbageCollect | ( | DdManager * | unique, |
| int | clearCache | ||
| ) |
Function********************************************************************
Synopsis [Performs garbage collection on the unique tables.]
Description [Performs garbage collection on the BDD and ZDD unique tables. If clearCache is 0, the cache is not cleared. This should only be specified if the cache has been cleared right before calling cuddGarbageCollect. (As in the case of dynamic reordering.) Returns the total number of deleted nodes.]
SideEffects [None]
SeeAlso []
Definition at line 20120 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the children of g.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 6196 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Fast storage allocation for items in a hash table.]
Description [Fast storage allocation for items in a hash table. The first 4 bytes of a chunk contain a pointer to the next block; the rest contains DD_MEM_CHUNK spaces for hash items. Returns a pointer to a new item if successful; NULL is memory is full.]
SideEffects [None]
SeeAlso [cuddAllocNode cuddDynamicAllocNode]
Definition at line 12494 of file cuddInt.c.
| int cuddHashTableGenericInsert | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| void * | value | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key is one pointer and the value is not a DdNode pointer. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert1 cuddHashTableGenericLookup]
Definition at line 11910 of file cuddInt.c.
| void* cuddHashTableGenericLookup | ( | DdHashTable * | hash, |
| DdNode * | f | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key consisting of one pointer in a hash table.]
Description [Looks up a key consisting of one pointer in a hash table when the value is not a DdNode pointer. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableLookup1 cuddHashTableGenericInsert]
Definition at line 11957 of file cuddInt.c.
| void cuddHashTableGenericQuit | ( | DdHashTable * | hash | ) |
Function********************************************************************
Synopsis [Shuts down a hash table.]
Description [Shuts down a hash table, when the values are not DdNode pointers.]
SideEffects [None]
SeeAlso [cuddHashTableInit]
Definition at line 11643 of file cuddInt.c.
| DdHashTable* cuddHashTableInit | ( | DdManager * | manager, |
| unsigned int | keySize, | ||
| unsigned int | initSize | ||
| ) |
Function********************************************************************
Synopsis [Initializes a hash table.]
Description [Initializes a hash table. Returns a pointer to the new table if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableQuit]
Definition at line 11548 of file cuddInt.c.
| int cuddHashTableInsert | ( | DdHashTable * | hash, |
| DdNodePtr * | key, | ||
| DdNode * | value, | ||
| ptrint | count | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key has more than three pointers. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [[cuddHashTableInsert1 cuddHashTableInsert2 cuddHashTableInsert3 cuddHashTableLookup]
Definition at line 11684 of file cuddInt.c.
| int cuddHashTableInsert1 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | value, | ||
| ptrint | count | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key is one pointer. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert cuddHashTableInsert2 cuddHashTableInsert3 cuddHashTableLookup1]
Definition at line 11803 of file cuddInt.c.
| int cuddHashTableInsert2 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | value, | ||
| ptrint | count | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key is composed of two pointers. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert3 cuddHashTableLookup2]
Definition at line 11996 of file cuddInt.c.
| int cuddHashTableInsert3 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | h, | ||
| DdNode * | value, | ||
| ptrint | count | ||
| ) |
Function********************************************************************
Synopsis [Inserts an item in a hash table.]
Description [Inserts an item in a hash table when the key is composed of three pointers. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert cuddHashTableInsert1 cuddHashTableInsert2 cuddHashTableLookup3]
Definition at line 12106 of file cuddInt.c.
| DdNode* cuddHashTableLookup | ( | DdHashTable * | hash, |
| DdNodePtr * | key | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key in a hash table.]
Description [Looks up a key consisting of more than three pointers in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.]
SideEffects [None]
SeeAlso [cuddHashTableLookup1 cuddHashTableLookup2 cuddHashTableLookup3 cuddHashTableInsert]
Definition at line 11739 of file cuddInt.c.
| DdNode* cuddHashTableLookup1 | ( | DdHashTable * | hash, |
| DdNode * | f | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key consisting of one pointer in a hash table.]
Description [Looks up a key consisting of one pointer in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.]
SideEffects [None]
SeeAlso [cuddHashTableLookup cuddHashTableLookup2 cuddHashTableLookup3 cuddHashTableInsert1]
Definition at line 11855 of file cuddInt.c.
| DdNode* cuddHashTableLookup2 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | g | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key consisting of two pointers in a hash table.]
Description [Looks up a key consisting of two pointer in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.]
SideEffects [None]
SeeAlso [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup3 cuddHashTableInsert2]
Definition at line 12050 of file cuddInt.c.
| DdNode* cuddHashTableLookup3 | ( | DdHashTable * | hash, |
| DdNode * | f, | ||
| DdNode * | g, | ||
| DdNode * | h | ||
| ) |
Function********************************************************************
Synopsis [Looks up a key consisting of three pointers in a hash table.]
Description [Looks up a key consisting of three pointers in a hash table. Returns the value associated to the key if there is an entry for the given key in the table; NULL otherwise. If the entry is present, its reference counter is decremented if not saturated. If the counter reaches 0, the value of the entry is dereferenced, and the entry is returned to the free list.]
SideEffects [None]
SeeAlso [cuddHashTableLookup cuddHashTableLookup1 cuddHashTableLookup2 cuddHashTableInsert3]
Definition at line 12162 of file cuddInt.c.
| void cuddHashTableQuit | ( | DdHashTable * | hash | ) |
Function********************************************************************
Synopsis [Shuts down a hash table.]
Description [Shuts down a hash table, dereferencing all the values.]
SideEffects [None]
SeeAlso [cuddHashTableInit]
Definition at line 11598 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Resizes a hash table.]
Description [Resizes a hash table. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddHashTableInsert]
Definition at line 12392 of file cuddInt.c.
| int cuddHeapProfile | ( | DdManager * | dd | ) |
Function********************************************************************
Synopsis [Prints information about the heap.]
Description [Prints to the manager's stdout the number of live nodes for each level of the DD heap that contains at least one live node. It also prints a summary containing:
If more than one table contains the maximum number of live nodes, only the one of lowest index is reported. Returns 1 in case of success and 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 5758 of file cuddInt.c.
| int cuddInitCache | ( | DdManager * | unique, |
| unsigned int | cacheSize, | ||
| unsigned int | maxCacheSize | ||
| ) |
CFile***********************************************************************
FileName [cuddCache.c]
PackageName [cudd]
Synopsis [Functions for cache insertion and lookup.]
Description [Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Initializes the computed table.]
Description [Initializes the computed table. It is called by Cudd_Init. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_Init]
| int cuddInitInteract | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Initializes the interaction matrix.]
Description [Initializes the interaction matrix. The interaction matrix is implemented as a bit vector storing the upper triangle of the symmetric interaction matrix. The bit vector is kept in an array of long integers. The computation is based on a series of depth-first searches, one for each root of the DAG. Two flags are needed: The local visited flag uses the LSB of the then pointer. The global visited flag uses the LSB of the next pointer. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 10963 of file cuddInt.c.
| int cuddInitLinear | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Initializes the linear transform matrix.]
Description [Initializes the linear transform matrix. Returns 1 if successful; 0 otherwise.]
SideEffects [none]
SeeAlso []
Definition at line 13269 of file cuddInt.c.
| DdManager* cuddInitTable | ( | unsigned int | numVars, |
| unsigned int | numVarsZ, | ||
| unsigned int | numSlots, | ||
| unsigned int | looseUpTo | ||
| ) |
Function********************************************************************
Synopsis [Creates and initializes the unique table.]
Description [Creates and initializes the unique table. Returns a pointer to the table if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_Init cuddFreeTable]
Definition at line 19738 of file cuddInt.c.
| int cuddLinearAndSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [BDD reduction based on combination of sifting and linear transformations.]
Description [BDD reduction based on combination of sifting and linear transformations. Assumes that no dead nodes are present.
Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 12750 of file cuddInt.c.
| int cuddLinearInPlace | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Linearly combines two adjacent variables.]
Description [Linearly combines two adjacent variables. Specifically, replaces the top variable with the exclusive nor of the two variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddLinearInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [The two subtables corrresponding to variables x and y are modified. The global counters of the unique table are also affected.]
SeeAlso [cuddSwapInPlace]
Definition at line 12874 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Inserts a local cache in the manager list.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 12333 of file cuddInt.c.
| void cuddLocalCacheClearAll | ( | DdManager * | manager | ) |
Function********************************************************************
Synopsis [Clears the local caches of a manager.]
Description [Clears the local caches of a manager. Used before reordering.]
SideEffects [None]
SeeAlso []
Definition at line 11414 of file cuddInt.c.
| void cuddLocalCacheClearDead | ( | DdManager * | manager | ) |
AutomaticEnd Function********************************************************************
Synopsis [Clears the dead entries of the local caches of a manager.]
Description [Clears the dead entries of the local caches of a manager. Used during garbage collection.]
SideEffects [None]
SeeAlso []
|
static |
Function********************************************************************
Synopsis [Removes a local cache from the manager list.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 12357 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Resizes a local cache.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 12222 of file cuddInt.c.
Function********************************************************************
Synopsis [Converts a ZDD cover to a BDD.]
Description [Converts a ZDD cover to a BDD. If successful, it returns a BDD node, otherwise it returns NULL. It is a recursive algorithm that works as follows. First it computes 3 cofactors of a ZDD cover: f1, f0 and fd. Second, it compute BDDs (b1, b0 and bd) of f1, f0 and fd. Third, it computes T=b1+bd and E=b0+bd. Fourth, it computes ITE(v,T,E) where v is the variable which has the index of the top node of the ZDD cover. In this case, since the index of v can be larger than either the one of T or the one of E, cuddUniqueInterIVO is called, where IVO stands for independent from variable ordering.]
SideEffects []
SeeAlso [Cudd_MakeBddFromZddCover]
Definition at line 28360 of file cuddInt.c.
| int cuddNextHigh | ( | DdManager * | table, |
| int | x | ||
| ) |
Function********************************************************************
Synopsis [Finds the next subtable with a larger index.]
Description [Finds the next subtable with a larger index. Returns the index.]
SideEffects [None]
SeeAlso [cuddNextLow]
| int cuddNextLow | ( | DdManager * | table, |
| int | x | ||
| ) |
Function********************************************************************
Synopsis [Finds the next subtable with a smaller index.]
Description [Finds the next subtable with a smaller index. Returns the index.]
SideEffects [None]
SeeAlso [cuddNextHigh]
Function********************************************************************
Synopsis [Recursively collects all the nodes of a DD in an array.]
Description [Traverses the DD f and collects all its nodes in an array. The caller should free the array returned by cuddNodeArray. Returns a pointer to the array of nodes in case of success; NULL otherwise. The nodes are collected in reverse topological order, so that a node is always preceded in the array by all its descendants.]
SideEffects [The number of nodes is returned as a side effect.]
SeeAlso [Cudd_FirstNode]
Definition at line 23067 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of cuddNodeArray.]
Description [Performs the recursive step of cuddNodeArray. Returns an the number of nodes in the DD. Clear the least significant bit of the next field that was used as visited flag by cuddNodeArrayRecur when counting the nodes. node is supposed to be regular; the invariant is maintained by this procedure.]
SideEffects [None]
SeeAlso []
Definition at line 23288 of file cuddInt.c.
| void cuddPrintNode | ( | DdNode * | f, |
| FILE * | fp | ||
| ) |
Function********************************************************************
Synopsis [Prints out information on a node.]
Description [Prints out information on a node.]
SideEffects [None]
SeeAlso []
Definition at line 5829 of file cuddInt.c.
Function********************************************************************
Synopsis [Prints the variable groups as a parenthesized list.]
Description [Prints the variable groups as a parenthesized list. For each group the level range that it represents is printed. After each group, the group's flags are printed, preceded by a `|'. For each flag (except MTR_TERMINAL) a character is printed.
The second argument, silent, if different from 0, causes Cudd_PrintVarGroups to only check the syntax of the group tree.]
SideEffects [None]
SeeAlso []
Function********************************************************************
Synopsis [Brings children of a dead node back.]
Description []
SideEffects [None]
SeeAlso [cuddReclaimZdd]
Definition at line 14223 of file cuddInt.c.
Function********************************************************************
Synopsis [Brings children of a dead ZDD node back.]
Description []
SideEffects [None]
SeeAlso [cuddReclaim]
Definition at line 14277 of file cuddInt.c.
| void cuddRehash | ( | DdManager * | unique, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [Rehashes a unique subtable.]
Description [Doubles the size of a unique subtable and rehashes its contents.]
SideEffects [None]
SeeAlso []
Definition at line 20917 of file cuddInt.c.
| int cuddResizeLinear | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Resizes the linear transform matrix.]
Description [Resizes the linear transform matrix. Returns 1 if successful; 0 otherwise.]
SideEffects [none]
SeeAlso []
Definition at line 13314 of file cuddInt.c.
| int cuddResizeTableZdd | ( | DdManager * | unique, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Increases the number of ZDD subtables in a unique table so that it meets or exceeds index.]
Description [Increases the number of ZDD subtables in a unique table so that it meets or exceeds index. When new ZDD variables are created, it is possible to preserve the functions unchanged, or it is possible to preserve the covers unchanged, but not both. cuddResizeTableZdd preserves the covers. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [ddResizeTable]
Definition at line 21093 of file cuddInt.c.
| void cuddSetInteract | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Set interaction matrix entries.]
Description [Given a pair of variables 0 <= x < y < table->size, sets the corresponding bit of the interaction matrix to 1.]
SideEffects [None]
SeeAlso []
Definition at line 10882 of file cuddInt.c.
| void cuddShrinkDeathRow | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Shrinks the death row.]
Description [Shrinks the death row by a factor of four.]
SideEffects [None]
SeeAlso [cuddClearDeathRow]
Definition at line 14327 of file cuddInt.c.
| int cuddSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Implementation of Rudell's sifting algorithm.]
Description [Implementation of Rudell's sifting algorithm. Assumes that no dead nodes are present.
Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 14824 of file cuddInt.c.
| void cuddSlowTableGrowth | ( | DdManager * | unique | ) |
| int cuddSwapInPlace | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Swaps two adjacent variables.]
Description [Swaps two adjacent variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddSwapInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
Definition at line 15082 of file cuddInt.c.
| int cuddSwapping | ( | DdManager * | table, |
| int | lower, | ||
| int | upper, | ||
| Cudd_ReorderingType | heuristic | ||
| ) |
Function********************************************************************
Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.]
Description [Implementation of Plessier's algorithm that reorders variables by a sequence of (non-adjacent) swaps.
Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 14926 of file cuddInt.c.
| int cuddSymmCheck | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Checks for symmetry of x and y.]
Description [Checks for symmetry of x and y. Ignores projection functions, unless they are isolated. Returns 1 in case of symmetry; 0 otherwise.]
SideEffects [None]
Definition at line 17912 of file cuddInt.c.
| int cuddSymmSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Symmetric sifting algorithm.]
Description [Symmetric sifting algorithm. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddSymmSiftingConv]
Definition at line 18042 of file cuddInt.c.
| int cuddSymmSiftingConv | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Symmetric sifting to convergence algorithm.]
Description [Symmetric sifting to convergence algorithm. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddSymmSifting]
Definition at line 18163 of file cuddInt.c.
| int cuddTestInteract | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Test interaction matrix entries.]
Description [Given a pair of variables 0 <= x < y < table->size, tests whether the corresponding bit of the interaction matrix is 1. Returns the value of the bit.]
SideEffects [None]
SeeAlso []
Definition at line 10917 of file cuddInt.c.
| int cuddTreeSifting | ( | DdManager * | table, |
| Cudd_ReorderingType | method | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Tree sifting algorithm.]
Description [Tree sifting algorithm. Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling ddTreeSiftingAux. Assumes that no dead nodes are present. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 8507 of file cuddInt.c.
| DdNode* cuddUniqueConst | ( | DdManager * | unique, |
| CUDD_VALUE_TYPE | value | ||
| ) |
Function********************************************************************
Synopsis [Checks the unique table for the existence of a constant node.]
Description [Checks the unique table for the existence of a constant node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. Returns a pointer to the new node.]
SideEffects [None]
Definition at line 20837 of file cuddInt.c.
Function********************************************************************
Synopsis [Checks the unique table for the existence of an internal node.]
Description [Checks the unique table for the existence of an internal node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. For a newly created node, increments the reference counts of what T and E point to. Returns a pointer to the new node if successful; NULL if memory is exhausted or if reordering took place.]
SideEffects [None]
SeeAlso [cuddUniqueInterZdd]
Definition at line 20495 of file cuddInt.c.
Function********************************************************************
Synopsis [Wrapper for cuddUniqueInter that is independent of variable ordering.]
Description [Wrapper for cuddUniqueInter that is independent of variable ordering (IVO). This function does not require parameter index to precede the indices of the top nodes of T and E in the variable order. Returns a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.]
SideEffects [None]
SeeAlso [cuddUniqueInter Cudd_MakeBddFromZddCover]
Definition at line 20691 of file cuddInt.c.
Function********************************************************************
Synopsis [Checks the unique table for the existence of an internal ZDD node.]
Description [Checks the unique table for the existence of an internal ZDD node. If it does not exist, it creates a new one. Does not modify the reference count of whatever is returned. A newly created internal node comes back with a reference count 0. For a newly created node, increments the reference counts of what T and E point to. Returns a pointer to the new node if successful; NULL if memory is exhausted or if reordering took place.]
SideEffects [None]
SeeAlso [cuddUniqueInter]
Definition at line 20730 of file cuddInt.c.
Function********************************************************************
Synopsis [Checks the unique table for the existence of an internal node.]
Description [Checks the unique table for the existence of an internal node. Returns a pointer to the node if it is in the table; NULL otherwise.]
SideEffects [None]
SeeAlso [cuddUniqueInter]
Definition at line 23428 of file cuddInt.c.
| void cuddUpdateInteractionMatrix | ( | DdManager * | table, |
| int | xindex, | ||
| int | yindex | ||
| ) |
| int cuddWindowReorder | ( | DdManager * | table, |
| int | low, | ||
| int | high, | ||
| Cudd_ReorderingType | submethod | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Reorders by applying the method of the sliding window.]
Description [Reorders by applying the method of the sliding window. Tries all possible permutations to the variables in a window that slides from low to high. The size of the window is determined by submethod. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 24123 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [XORs two rows of the linear transform matrix.]
Description [XORs two rows of the linear transform matrix and replaces the first row with the result.]
SideEffects [none]
SeeAlso []
Definition at line 13863 of file cuddInt.c.
| int cuddZddAlignToBdd | ( | DdManager * | table | ) |
Function********************************************************************
Synopsis [Reorders ZDD variables according to the order of the BDD variables.]
Description [Reorders ZDD variables according to the order of the BDD variables. This function can be called at the end of BDD reordering to insure that the order of the ZDD variables is consistent with the order of the BDD variables. The number of ZDD variables must be a multiple of the number of BDD variables. Let M be the ratio of the two numbers. cuddZddAlignToBdd then considers the ZDD variables from M*i to (M+1)*i-1 as corresponding to BDD variable i. This function should be normally called from Cudd_ReduceHeap, which clears the cache. Returns 1 in case of success; 0 otherwise.]
SideEffects [Changes the ZDD variable order for all diagrams and performs garbage collection of the ZDD unique table.]
SeeAlso [Cudd_zddShuffleHeap Cudd_ReduceHeap]
Definition at line 29753 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddChange.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 31650 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes a complement of a ZDD node.]
Description [Computes the complement of a ZDD node. So far, since we couldn't find a direct way to get the complement of a ZDD cover, we first convert a ZDD cover to a BDD, then make the complement of the ZDD cover from the complement of the BDD node by using ISOP.]
SideEffects [The result depends on current variable order.]
SeeAlso []
Definition at line 26289 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDiff.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 31568 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivide.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivide]
Definition at line 25926 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddDivideF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddDivideF]
Definition at line 26026 of file cuddInt.c.
| void cuddZddFreeUniv | ( | DdManager * | zdd | ) |
Function********************************************************************
Synopsis [Frees the ZDD universe.]
Description [Frees the ZDD universe.]
SideEffects [None]
SeeAlso [cuddZddInitUniv]
Definition at line 10717 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the two-way decomposition of f w.r.t. v.]
Description []
SideEffects [The results are returned in f1 and f0.]
SeeAlso [cuddZddGetCofactors3]
Definition at line 26254 of file cuddInt.c.
| int cuddZddGetCofactors3 | ( | DdManager * | dd, |
| DdNode * | f, | ||
| int | v, | ||
| DdNode ** | f1, | ||
| DdNode ** | f0, | ||
| DdNode ** | fd | ||
| ) |
Function********************************************************************
Synopsis [Computes the three-way decomposition of f w.r.t. v.]
Description [Computes the three-way decomposition of function f (represented by a ZDD) wit respect to variable v. Returns 0 if successful; 1 otherwise.]
SideEffects [The results are returned in f1, f0, and fd.]
SeeAlso [cuddZddGetCofactors2]
Definition at line 26127 of file cuddInt.c.
| int cuddZddGetNegVarIndex | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Returns the index of negative ZDD variable.]
Description [Returns the index of negative ZDD variable.]
SideEffects []
SeeAlso []
| int cuddZddGetNegVarLevel | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Wrapper for cuddUniqueInterZdd.]
Description [Wrapper for cuddUniqueInterZdd, which applies the ZDD reduction rule. Returns a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.]
SideEffects [None]
SeeAlso [cuddUniqueInterZdd]
Definition at line 20408 of file cuddInt.c.
Function********************************************************************
Synopsis [Wrapper for cuddUniqueInterZdd that is independent of variable ordering.]
Description [Wrapper for cuddUniqueInterZdd that is independent of variable ordering (IVO). This function does not require parameter index to precede the indices of the top nodes of g and h in the variable order. Returns a pointer to the result node under normal conditions; NULL if reordering occurred or memory was exhausted.]
SideEffects [None]
SeeAlso [cuddZddGetNode cuddZddIsop]
Definition at line 20441 of file cuddInt.c.
| int cuddZddGetPosVarIndex | ( | DdManager * | dd, |
| int | index | ||
| ) |
Function********************************************************************
Synopsis [Returns the index of positive ZDD variable.]
Description [Returns the index of positive ZDD variable.]
SideEffects []
SeeAlso []
| int cuddZddGetPosVarLevel | ( | DdManager * | dd, |
| int | index | ||
| ) |
| int cuddZddInitUniv | ( | DdManager * | zdd | ) |
Function********************************************************************
Synopsis [Initializes the ZDD universe.]
Description [Initializes the ZDD universe. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddZddFreeUniv]
Definition at line 10668 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIntersect.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 31493 of file cuddInt.c.
CFile***********************************************************************
FileName [cuddZddIsop.c]
PackageName [cudd]
Synopsis [Functions to find irredundant SOP covers as ZDDs from BDDs.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [In-Ho Moon]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIsop.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddIsop]
Definition at line 27794 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddIte.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 31278 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]
Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. Finds the best position and does the required changes. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 29050 of file cuddInt.c.
Function********************************************************************
Synopsis [Given a set of moves, returns the ZDD heap to the position giving the minimum size.]
Description [Given a set of moves, returns the ZDD heap to the position giving the minimum size. In case of ties, returns to the closest position giving the minimum size. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 29346 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts a variable down and applies the XOR transformation.]
Description [Sifts a variable down. Moves x down until either it reaches the bound (xHigh) or the size of the ZDD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
SeeAlso []
Definition at line 29262 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Linearly combines two adjacent variables.]
Description [Linearly combines two adjacent variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddZddLinearInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddZddSwapInPlace cuddLinearInPlace]
Definition at line 28728 of file cuddInt.c.
| int cuddZddLinearSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Implementation of the linear sifting algorithm for ZDDs.]
Description [Implementation of the linear sifting algorithm for ZDDs. Assumes that no dead nodes are present.
Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 28625 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts a variable up applying the XOR transformation.]
Description [Sifts a variable up applying the XOR transformation. Moves y up until either it reaches the bound (xLow) or the size of the ZDD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
SeeAlso []
Definition at line 29177 of file cuddInt.c.
| int cuddZddNextHigh | ( | DdManager * | table, |
| int | x | ||
| ) |
Function********************************************************************
Synopsis [Finds the next subtable with a larger index.]
Description [Finds the next subtable with a larger index. Returns the index.]
SideEffects [None]
SeeAlso []
| int cuddZddNextLow | ( | DdManager * | table, |
| int | x | ||
| ) |
Function********************************************************************
Synopsis [Finds the next subtable with a smaller index.]
Description [Finds the next subtable with a smaller index. Returns the index.]
SideEffects [None]
SeeAlso []
CFile***********************************************************************
FileName [cuddZddFuncs.c]
PackageName [cudd]
Synopsis [Functions to manipulate covers represented as ZDDs.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [In-Ho Moon]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddProduct]
Definition at line 25147 of file cuddInt.c.
| int cuddZddSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Implementation of Rudell's sifting algorithm.]
Description [Implementation of Rudell's sifting algorithm. Assumes that no dead nodes are present.
Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 30268 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]
Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. Finds the best position and does the required changes. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 30522 of file cuddInt.c.
Function********************************************************************
Synopsis [Given a set of moves, returns the ZDD heap to the position giving the minimum size.]
Description [Given a set of moves, returns the ZDD heap to the position giving the minimum size. In case of ties, returns to the closest position giving the minimum size. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 30769 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts a variable down.]
Description [Sifts a variable down. Moves x down until either it reaches the bound (x_high) or the size of the ZDD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
SeeAlso []
Definition at line 30705 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts a variable up.]
Description [Sifts a variable up. Moves y up until either it reaches the bound (x_low) or the size of the ZDD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
SeeAlso []
Definition at line 30642 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]
Description [Computes the negative cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is negated. Returns a pointer to the result if successful; NULL otherwise. cuddZddSubset0 performs the same function as Cudd_zddSubset0, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.]
SideEffects [None]
SeeAlso [cuddZddSubset1 Cudd_zddSubset0]
Definition at line 31774 of file cuddInt.c.
Function********************************************************************
Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]
Description [Computes the positive cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is asserted. Returns a pointer to the result if successful; NULL otherwise. cuddZddSubset1 performs the same function as Cudd_zddSubset1, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.]
SideEffects [None]
SeeAlso [cuddZddSubset0 Cudd_zddSubset1]
Definition at line 31725 of file cuddInt.c.
| int cuddZddSwapInPlace | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
Function********************************************************************
Synopsis [Swaps two adjacent variables.]
Description [Swaps two adjacent variables. It assumes that no dead nodes are present on entry to this procedure. The procedure then guarantees that no dead nodes will be present when it terminates. cuddZddSwapInPlace assumes that x < y. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 29885 of file cuddInt.c.
| int cuddZddSwapping | ( | DdManager * | table, |
| int | lower, | ||
| int | upper, | ||
| Cudd_ReorderingType | heuristic | ||
| ) |
Function********************************************************************
Synopsis [Reorders variables by a sequence of (non-adjacent) swaps.]
Description [Implementation of Plessier's algorithm that reorders variables by a sequence of (non-adjacent) swaps.
Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 30147 of file cuddInt.c.
| int cuddZddSymmCheck | ( | DdManager * | table, |
| int | x, | ||
| int | y | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Checks for symmetry of x and y.]
Description [Checks for symmetry of x and y. Ignores projection functions, unless they are isolated. Returns 1 in case of symmetry; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 32127 of file cuddInt.c.
| int cuddZddSymmSifting | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Symmetric sifting algorithm for ZDDs.]
Description [Symmetric sifting algorithm. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddZddSymmSiftingConv]
Definition at line 32232 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Moves x down until either it reaches the bound (x_high) or the size of the ZDD heap increases too much.]
Description [Moves x down until either it reaches the bound (x_high) or the size of the ZDD heap increases too much. Assumes that x is the bottom of a symmetry group. Checks x for symmetry to the adjacent variables. If symmetry is found, the symmetry group of x is merged with the symmetry group of the other variable. Returns the set of moves in case of success; ZDD_MV_OOM if memory is full.]
SideEffects [None]
SeeAlso []
Definition at line 33280 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Moves x up until either it reaches the bound (x_low) or the size of the ZDD heap increases too much.]
Description [Moves x up until either it reaches the bound (x_low) or the size of the ZDD heap increases too much. Assumes that x is the top of a symmetry group. Checks x for symmetry to the adjacent variables. If symmetry is found, the symmetry group of x is merged with the symmetry group of the other variable. Returns the set of moves in case of success; ZDD_MV_OOM if memory is full.]
SideEffects [None]
SeeAlso []
Definition at line 33192 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Given x_low <= x <= x_high moves x up and down between the boundaries.]
Description [Given x_low <= x <= x_high moves x up and down between the boundaries. Finds the best position and does the required changes. Assumes that x is not part of a symmetry group. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 32543 of file cuddInt.c.
Function********************************************************************
Synopsis [Given a set of moves, returns the ZDD heap to the position giving the minimum size.]
Description [Given a set of moves, returns the ZDD heap to the position giving the minimum size. In case of ties, returns to the closest position giving the minimum size. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 33371 of file cuddInt.c.
| int cuddZddSymmSiftingConv | ( | DdManager * | table, |
| int | lower, | ||
| int | upper | ||
| ) |
Function********************************************************************
Synopsis [Symmetric sifting to convergence algorithm for ZDDs.]
Description [Symmetric sifting to convergence algorithm for ZDDs. Assumes that no dead nodes are present.
Returns 1 plus the number of symmetric variables if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [cuddZddSymmSifting]
Definition at line 32357 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Given x_low <= x <= x_high moves x up and down between the boundaries.]
Description [Given x_low <= x <= x_high moves x up and down between the boundaries. Finds the best position and does the required changes. Assumes that x is either an isolated variable, or it is the bottom of a symmetry group. All symmetries may not have been found, because of exceeded growth limit. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 32883 of file cuddInt.c.
|
static |
| int cuddZddTreeSifting | ( | DdManager * | table, |
| Cudd_ReorderingType | method | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Tree sifting algorithm for ZDDs.]
Description [Tree sifting algorithm for ZDDs. Assumes that a tree representing a group hierarchy is passed as a parameter. It then reorders each group in postorder fashion by calling zddTreeSiftingAux. Assumes that no dead nodes are present. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 26558 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddUnateProduct.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddUnateProduct]
Definition at line 25384 of file cuddInt.c.
Function********************************************************************
Synopsis [Given a set of moves, returns the ZDD heap to the order in effect before the moves.]
Description [Given a set of moves, returns the ZDD heap to the order in effect before the moves. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 29394 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddUnion.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 31404 of file cuddInt.c.
| int cuddZddUniqueCompare | ( | int * | ptr_x, |
| int * | ptr_y | ||
| ) |
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.]
SideEffects [None]
SeeAlso []
Definition at line 29860 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDiv.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDiv]
Definition at line 25528 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddWeakDivF.]
Description []
SideEffects [None]
SeeAlso [Cudd_zddWeakDivF]
Definition at line 25689 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddMaximallyExpand.]
Description [Performs the recursive step of Cudd_bddMaximallyExpand. Returns set of primes or zero BDD if successful; NULL otherwise. On entry to this function, ub and lb should be different from the zero BDD. The function then maintains this invariant.]
SideEffects [None]
SeeAlso []
There are three major terminal cases in theory: ub -> f : return ub lb == f : return lb not(lb -> f): return zero Only the second case can be checked exactly in constant time. For the others, we check for sufficient conditions.
Definition at line 17521 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Performs shortest path computation on a unate function.]
Description [Performs shortest path computation on a unate function. Returns the length of the shortest path to one if successful; CUDD_OUT_OF_MEM otherwise. This function is based on the observation that in the BDD of a unate function no node except the constant is reachable from the root via paths of different parity.]
SideEffects [None]
SeeAlso [getShortest]
Definition at line 17730 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Checks the BDD variable group tree before a shuffle.]
Description [Checks the BDD variable group tree before a shuffle. Returns 1 if successful; 0 otherwise.]
SideEffects [Changes the BDD variable group tree.]
SeeAlso []
Definition at line 16424 of file cuddInt.c.
|
static |
|
static |
Function********************************************************************
Synopsis [Scans the DD and clears the LSB of the next pointers.]
Description [Scans the DD and clears the LSB of the next pointers. The LSB of the next pointers are used as markers to tell whether a node was reached. Once the roots are counted, these flags are reset.]
SideEffects [None]
SeeAlso [ddCountRoots]
Definition at line 7088 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Scans the DD and clears the LSB of the next pointers.]
Description [The LSB of the next pointers are used as markers to tell whether a node was reached by at least one DFS. Once the interaction matrix is built, these flags are reset.]
SideEffects [None]
SeeAlso []
Definition at line 11139 of file cuddInt.c.
|
static |
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_CountMinterm.]
Description [Performs the recursive step of Cudd_CountMinterm. It is based on the following identity. Let |f| be the number of minterms of f. Then: <xmp> |f| = (|f0|+|f1|)/2 </xmp> where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff. Returns the number of minterms of the function rooted at node.]
SideEffects [None]
Definition at line 23527 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_CountPath.]
Description [Performs the recursive step of Cudd_CountPath. It is based on the following identity. Let |f| be the number of paths of f. Then: <xmp> |f| = |f0|+|f1| </xmp> where f0 and f1 are the two cofactors of f. Uses the identity |f'| = |f|, to improve the utilization of the (local) cache. Returns the number of paths of the function rooted at node.]
SideEffects [None]
Definition at line 23600 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_CountPathsToNonZero.]
Description [Performs the recursive step of Cudd_CountPathsToNonZero. It is based on the following identity. Let |f| be the number of paths of f. Then: <xmp> |f| = |f0|+|f1| </xmp> where f0 and f1 are the two cofactors of f. Returns the number of paths of the function rooted at node.]
SideEffects [None]
Definition at line 23733 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Counts the number of roots.]
Description [Counts the number of roots at the levels between lower and upper. The computation is based on breadth-first search. A node is a root if it is not reachable from any previously visited node. (All the nodes at level lower are therefore considered roots.) The visited flag uses the LSB of the next pointer. Returns the root count. The roots that are constant nodes are always ignored.]
SideEffects [None]
SeeAlso [ddClearGlobal]
Definition at line 7021 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Creates a group encompassing variables from x to y in the DD table.]
Description [Creates a group encompassing variables from x to y in the DD table. In the current implementation it must be y == x+1. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 9156 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_DagSize.]
Description [Performs the recursive step of Cudd_DagSize. Returns the number of nodes in the graph rooted at n.]
SideEffects [None]
Definition at line 23253 of file cuddInt.c.
|
static |
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_EpdCountMinterm.]
Description [Performs the recursive step of Cudd_EpdCountMinterm. It is based on the following identity. Let |f| be the number of minterms of f. Then: <xmp> |f| = (|f0|+|f1|)/2 </xmp> where f0 and f1 are the two cofactors of f. Does not use the identity |f'| = max - |f|, to minimize loss of accuracy due to roundoff. Returns the number of minterms of the function rooted at node.]
SideEffects [None]
Definition at line 23661 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [This function is for exchanging two variables, x and y.]
Description [This is the same funcion as ddSwapping except for comparison expression. Use probability function, exp(-size_change/temp).]
SideEffects [None]
SeeAlso []
Definition at line 962 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Checks for extended symmetry of x and y.]
Description [Checks for extended symmetry of x and y. Returns 1 in case of extended symmetry; 0 otherwise.]
SideEffects [None]
Definition at line 10179 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Finds the lower and upper bounds of the group represented by treenode.]
Description [Finds the lower and upper bounds of the group represented by treenode. From the index and size fields we need to derive the current positions, and find maximum and minimum.]
SideEffects [The bounds are returned as side effects.]
SeeAlso []
Definition at line 8853 of file cuddInt.c.
Function********************************************************************
Synopsis [Recursively find the support of f.]
Description [Recursively find the support of f. This function uses the LSB of the next field of the nodes of f as visited flag. It also uses the LSB of the next field of the variables as flag to remember whether a certain index has already been seen. Finally, it uses the manager stack to record all seen indices.]
SideEffects [The stack pointer SP is modified by side-effect. The next fields are changed and need to be reset.]
Definition at line 23953 of file cuddInt.c.
Function********************************************************************
Synopsis [Adjusts the values of table limits.]
Description [Adjusts the values of table fields controlling the. sizes of subtables and computed table. If the computed table is too small according to the new values, it is resized.]
SideEffects [Modifies manager fields. May resize computed table.]
SeeAlso []
Definition at line 21624 of file cuddInt.c.
Function********************************************************************
Synopsis [Swaps two groups and records the move.]
Description [Swaps two groups and records the move. Returns the number of keys in the DD table in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 9729 of file cuddInt.c.
|
static |
|
static |
Function********************************************************************
Synopsis [Sifts from treenode->low to treenode->high.]
Description [Sifts from treenode->low to treenode->high. If croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the end of the initial sifting. If a group is created, it is then sifted again. After sifting one variable, the group that contains it is dissolved. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 8956 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Sifts one variable up and down until it has taken all positions. Checks for aggregation.]
Description [Sifts one variable up and down until it has taken all positions. Checks for aggregation. There may be at most two sweeps, even if the group grows. Assumes that x is either an isolated variable, or it is the bottom of a group. All groups may not have been found. The variable being moved is returned to the best position seen during sifting. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 9197 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Determines the best position for a variables and returns it there.]
Description [Determines the best position for a variables and returns it there. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 9909 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Sifts down a variable until it reaches position xHigh.]
Description [Sifts down a variable until it reaches position xHigh. Assumes that x is the bottom of a group (or a singleton). Records all the moves. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 9553 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.]
Description [Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much. Assumes that y is the top of a group (or a singleton). Checks y for aggregation to the adjacent variables. Records all the moves that are appended to the list of moves received as input and returned as a side effect. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 9395 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Checks whether a variables is already handled.]
Description [Checks whether a variables is already handled. This function is used for lazy sifting.]
SideEffects [none]
SeeAlso []
Definition at line 10417 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Moves a variable to a specified position.]
Description [If x==x_low, it executes jumping_down. If x==x_high, it executes jumping_up. This funcion is similar to ddSiftingAux. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 1111 of file cuddInt.c.
Function********************************************************************
Synopsis [This function is for jumping down.]
Description [This is a simplified version of ddSiftingDown. It does not use lower bounding. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
SeeAlso []
Definition at line 1241 of file cuddInt.c.
Function********************************************************************
Synopsis [This function is for jumping up.]
Description [This is a simplified version of ddSiftingUp. It does not use lower bounding. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
SeeAlso []
Definition at line 1182 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_CountLeaves.]
Description [Performs the recursive step of Cudd_CountLeaves. Returns the number of leaves in the DD rooted at n.]
SideEffects [None]
SeeAlso [Cudd_CountLeaves]
Definition at line 23852 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]
Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. At each step a linear transformation is tried, and, if it decreases the size of the DD, it is accepted. Finds the best position and does the required changes. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 13410 of file cuddInt.c.
Function********************************************************************
Synopsis [Given a set of moves, returns the DD heap to the order giving the minimum size.]
Description [Given a set of moves, returns the DD heap to the position giving the minimum size. In case of ties, returns to the closest position giving the minimum size. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 13752 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Sifts a variable down and applies linear transformations.]
Description [Sifts a variable down and applies linear transformations. Moves x down until either it reaches the bound (xHigh) or the size of the DD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
Definition at line 13639 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts a variable up and applies linear transformations.]
Description [Sifts a variable up and applies linear transformations. Moves y up until either it reaches the bound (xLow) or the size of the DD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
Definition at line 13516 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.]
SideEffects [None]
|
static |
Function********************************************************************
Synopsis [Pretends to check two variables for aggregation.]
Description [Pretends to check two variables for aggregation. Always returns 0.]
SideEffects [None]
Function********************************************************************
Synopsis [Fixes a variable tree after the insertion of new subtables.]
Description [Fixes a variable tree after the insertion of new subtables. After such an insertion, the low fields of the tree below the insertion point are inconsistent.]
SideEffects [None]
SeeAlso []
Definition at line 21899 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Tries all the permutations of the three variables between x and x+2 and retains the best.]
Description [Tries all the permutations of the three variables between x and x+2 and retains the best. Assumes that no dead nodes are present. Returns the index of the best permutation (1-6) in case of success; 0 otherwise.Assumes that no dead nodes are present. Returns the index of the best permutation (1-6) in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 24342 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Tries all the permutations of the four variables between w and w+3 and retains the best.]
Description [Tries all the permutations of the four variables between w and w+3 and retains the best. Assumes that no dead nodes are present. Returns the index of the best permutation (1-24) in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 24582 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_bddPickArbitraryMinterms.]
Description [Performs the recursive step of Cudd_bddPickArbitraryMinterms. Returns 1 if successful; 0 otherwise.]
SideEffects [none]
SeeAlso [Cudd_bddPickArbitraryMinterms]
Definition at line 23884 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_PrintMinterm.]
Description []
SideEffects [None]
Definition at line 23199 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Rehashes a ZDD unique subtable.]
Description []
SideEffects [None]
SeeAlso [cuddRehash]
Definition at line 21274 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders the children of a group tree node according to the options.]
Description [Reorders the children of a group tree node according to the options. After reordering puts all the variables in the group and/or its descendents in a single group. This allows hierarchical reordering. If the variables in the group do not exist yet, simply does nothing. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 8689 of file cuddInt.c.
|
static |
|
static |
Function********************************************************************
Synopsis [Prepares the DD heap for dynamic reordering.]
Description [Prepares the DD heap for dynamic reordering. Does garbage collection, to guarantee that there are no dead nodes; clears the cache, which is invalidated by dynamic reordering; initializes the number of isolated projection functions; and initializes the interaction matrix. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 16147 of file cuddInt.c.
|
static |
|
static |
|
static |
Function********************************************************************
Synopsis [Increases the number of subtables in a unique table so that it meets or exceeds index.]
Description [Increases the number of subtables in a unique table so that it meets or exceeds index. The parameter amount determines how much spare space is allocated to prevent too frequent resizing. If index is negative, the table is resized, but no new variables are created. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso [Cudd_Reserve cuddResizeTableZdd]
Definition at line 21378 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Checks two variables for aggregation.]
Description [Checks two variables for aggregation. The check is based on the second difference of the number of nodes as a function of the layer. If the second difference is lower than a given threshold (typically negative) then the two variables should be aggregated. Returns 1 if the two variables pass the test; 0 otherwise.]
SideEffects [None]
Definition at line 10122 of file cuddInt.c.
|
static |
|
static |
Function********************************************************************
Synopsis [Reorders variables according to a given permutation.]
Description [Reorders variables according to a given permutation. The i-th permutation array contains the index of the variable that should be brought to the i-th level. ddShuffle assumes that no dead nodes are present and that the interaction matrix is properly initialized. The reordering is achieved by a series of upward sifts. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 6862 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders variables according to a given permutation.]
Description [Reorders variables according to a given permutation. The i-th permutation array contains the index of the variable that should be brought to the i-th level. ddShuffle assumes that no dead nodes are present and that the interaction matrix is properly initialized. The reordering is achieved by a series of upward sifts. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 16218 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]
Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. Finds the best position and does the required changes. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 15809 of file cuddInt.c.
Function********************************************************************
Synopsis [Given a set of moves, returns the DD heap to the position giving the minimum size.]
Description [Given a set of moves, returns the DD heap to the position giving the minimum size. In case of ties, returns to the closest position giving the minimum size. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 16108 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts a variable down.]
Description [Sifts a variable down. Moves x down until either it reaches the bound (xHigh) or the size of the DD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
Definition at line 16016 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts a variable up.]
Description [Sifts a variable up. Moves y up until either it reaches the bound (xLow) or the size of the DD heap increases too much. Returns the set of moves in case of success; NULL if memory is full.]
SideEffects [None]
Definition at line 15916 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Moves one variable up.]
Description [Takes a variable from position x and sifts it up to position xLow; xLow should be less than or equal to x. Returns 1 if successful; 0 otherwise]
SideEffects [None]
SeeAlso []
Definition at line 6944 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Moves one variable up.]
Description [Takes a variable from position x and sifts it up to position xLow; xLow should be less than or equal to x. Returns 1 if successful; 0 otherwise]
SideEffects [None]
SeeAlso []
Definition at line 16295 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Find the support of f.]
Description [Performs a DFS from f. Uses the LSB of the then pointer as visited flag.]
SideEffects [Accumulates in support the variables on which f depends.]
SeeAlso []
Definition at line 11043 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_Support.]
Description [Performs the recursive step of Cudd_Support. Performs a DFS from f. The support is accumulated in supp as a side effect. Uses the LSB of the then pointer as visited flag.]
SideEffects [None]
SeeAlso [ddClearFlag]
Definition at line 23792 of file cuddInt.c.
Function********************************************************************
Synopsis [Swaps any two variables.]
Description [Swaps any two variables. Returns the set of moves.]
SideEffects [None]
Definition at line 15668 of file cuddInt.c.
Function********************************************************************
Synopsis [Swaps two groups.]
Description [Swaps two groups. x is assumed to be the bottom variable of the first group. y is assumed to be the top variable of the second group. Updates the list of moves. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
Definition at line 19204 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Undoes the swap of two groups.]
Description [Undoes the swap of two groups. x is assumed to be the bottom variable of the first group. y is assumed to be the top variable of the second group. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
Definition at line 19285 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]
Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. Finds the best position and does the required changes. Assumes that x is not part of a symmetry group. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 18365 of file cuddInt.c.
Function********************************************************************
Synopsis [Given a set of moves, returns the DD heap to the position giving the minimum size.]
Description [Given a set of moves, returns the DD heap to the position giving the minimum size. In case of ties, returns to the closest position giving the minimum size. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 19356 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Given xLow <= x <= xHigh moves x up and down between the boundaries.]
Description [Given xLow <= x <= xHigh moves x up and down between the boundaries. Finds the best position and does the required changes. Assumes that x is either an isolated variable, or it is the bottom of a symmetry group. All symmetries may not have been found, because of exceeded growth limit. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 18667 of file cuddInt.c.
Function********************************************************************
Synopsis [Moves x down until either it reaches the bound (xHigh) or the size of the DD heap increases too much.]
Description [Moves x down until either it reaches the bound (xHigh) or the size of the DD heap increases too much. Assumes that x is the bottom of a symmetry group. Checks x for symmetry to the adjacent variables. If symmetry is found, the symmetry group of x is merged with the symmetry group of the other variable. Returns the set of moves in case of success; MV_OOM if memory is full.]
SideEffects [None]
Definition at line 19066 of file cuddInt.c.
Function********************************************************************
Synopsis [Moves x up until either it reaches the bound (xLow) or the size of the DD heap increases too much.]
Description [Moves x up until either it reaches the bound (xLow) or the size of the DD heap increases too much. Assumes that x is the top of a symmetry group. Checks x for symmetry to the adjacent variables. If symmetry is found, the symmetry group of x is merged with the symmetry group of the other variable. Returns the set of moves in case of success; MV_OOM if memory is full.]
SideEffects [None]
Definition at line 18924 of file cuddInt.c.
|
static |
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.]
SideEffects [None]
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Visits the group tree and reorders each group.]
Description [Recursively visits the group tree and reorders each group in postorder fashion. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 8597 of file cuddInt.c.
Function********************************************************************
Synopsis [Given a set of moves, returns the DD heap to the order in effect before the moves.]
Description [Given a set of moves, returns the DD heap to the order in effect before the moves. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 13798 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.]
SideEffects [None]
|
static |
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.]
SideEffects [None]
|
static |
Function********************************************************************
Synopsis [Marks as interacting all pairs of variables that appear in support.]
Description [If support[i] == support[j] == 1, sets the (i,j) entry of the interaction matrix to 1.]
SideEffects [Clears support.]
SeeAlso []
Definition at line 11103 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Updates the BDD variable group tree before a shuffle.]
Description [Updates the BDD variable group tree before a shuffle. Returns 1 if successful; 0 otherwise.]
SideEffects [Changes the BDD variable group tree.]
SeeAlso []
Definition at line 16365 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Checks for grouping of x and y.]
Description [Checks for grouping of x and y. Returns 1 in case of grouping; 0 otherwise. This function is used for lazy sifting.]
SideEffects [None]
Definition at line 10329 of file cuddInt.c.
|
static |
CFile***********************************************************************
FileName [cuddWindow.c]
PackageName [cudd]
Synopsis [Functions for variable reordering by window permutation.]
Description [Internal procedures included in this module:
Static procedures included in this module:
]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart
Function********************************************************************
Synopsis [Reorders by applying a sliding window of width 2.]
Description [Reorders by applying a sliding window of width 2. Tries both permutations of the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 24195 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders by applying a sliding window of width 3.]
Description [Reorders by applying a sliding window of width 3. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 24437 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders by applying a sliding window of width 4.]
Description [Reorders by applying a sliding window of width 4. Tries all possible permutations to the variables in a window that slides from low to high. Assumes that no dead nodes are present. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 24838 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders by repeatedly applying a sliding window of width 2.]
Description [Reorders by repeatedly applying a sliding window of width
SideEffects [None]
Definition at line 24249 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders by repeatedly applying a sliding window of width 3.]
Description [Reorders by repeatedly applying a sliding window of width
SideEffects [None]
Definition at line 24484 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders by repeatedly applying a sliding window of width 4.]
Description [Reorders by repeatedly applying a sliding window of width
SideEffects [None]
Definition at line 24885 of file cuddInt.c.
CFile***********************************************************************
FileName [cuddCheck.c]
PackageName [cudd]
Synopsis [Functions to check consistency of data structures.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart
Function********************************************************************
Synopsis [Searches the subtables above node for its parents.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 5929 of file cuddInt.c.
AutomaticStart
Function********************************************************************
Synopsis [Performs the recursive step of cuddP.]
Description [Performs the recursive step of cuddP. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 23106 of file cuddInt.c.
|
static |
|
static |
CFile***********************************************************************
FileName [cuddAPI.c]
PackageName [cudd]
Synopsis [Application interface functions.]
Description [External procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart
Function********************************************************************
Synopsis [Fixes a variable group tree.]
Description []
SideEffects [Changes the variable group tree.]
SeeAlso []
Definition at line 2126 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Frees a two-dimensional matrix allocated by getMatrix.]
Description []
SideEffects [None]
SeeAlso [getMatrix]
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Frees the entries of the visited symbol table.]
Description [Frees the entries of the visited symbol table. Returns ST_CONTINUE.]
SideEffects [None]
Definition at line 17213 of file cuddInt.c.
Function********************************************************************
Synopsis [Build a BDD for a largest cube of f.]
Description [Build a BDD for a largest cube of f. Given the minimum length from the root, and the minimum lengths for each node (in visited), apply triangulation at each node. Of the two children of each node on a shortest path, at least one is on a shortest path. In case of ties the procedure chooses the THEN children. Returns a pointer to the cube BDD representing the path if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 17435 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Finds the size of the largest cube(s) in a DD.]
Description [Finds the size of the largest cube(s) in a DD. This problem is translated into finding the shortest paths from a node when both THEN and ELSE arcs have unit lengths. Uses a local symbol table to store the lengths for each node. Only the lengths for the regular nodes are entered in the table, because those for the complement nodes are simply obtained by swapping the two lenghts. Returns a pair of lengths: the length of the shortest path to 1; and the length of the shortest path to 0. This is done so as to take complement arcs into account.]
SideEffects [none]
SeeAlso []
Definition at line 17347 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Returns the number of nodes at one level of a unique table.]
Description [Returns the number of nodes at one level of a unique table. The projection function, if isolated, is not counted.]
SideEffects [None]
SeeAlso []
Definition at line 6830 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Allocates a two-dimensional matrix of ints.]
Description [Allocates a two-dimensional matrix of ints. Returns the pointer to the matrix if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [freeMatrix]
Definition at line 6772 of file cuddInt.c.
|
static |
CFile***********************************************************************
FileName [cuddExact.c]
PackageName [cudd]
Synopsis [Functions for exact variable reordering.]
Description [External procedures included in this file:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Cheng Hua, Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart
Function********************************************************************
Synopsis [Returns the maximum value of (n choose k) for a given n.]
Description [Computes the maximum value of (n choose k) for a given n. The maximum value occurs for k = n/2 when n is even, or k = (n-1)/2 when n is odd. The algorithm used in this procedure avoids intermediate overflow problems. It is based on the identity
binomial(n,k) = n/k * binomial(n-1,k-1).
Returns the computed value if successful; -1 if out of range.]
SideEffects [None]
SeeAlso []
Definition at line 6684 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Finds the length of the shortest path(s) in a DD.]
Description [Finds the length of the shortest path(s) in a DD. Uses a local symbol table to store the lengths for each node. Only the lengths for the regular nodes are entered in the table, because those for the complement nodes are simply obtained by swapping the two lenghts. Returns a pair of lengths: the length of the shortest path to 1; and the length of the shortest path to 0. This is done so as to take complement arcs into account.]
SideEffects [Accumulates the support of the DD in support.]
SeeAlso []
Definition at line 17246 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Gathers symmetry information.]
Description [Translates the symmetry information stored in the next field of each subtable from level to indices. This procedure is called immediately after symmetric sifting, so that the next fields are correct. By translating this informaton in terms of indices, we make it independent of subsequent reorderings. The format used is that of the next fields: a circular list where each variable points to the next variable in the same symmetry group. Only the entries between lower and upper are considered. The procedure returns a pointer to an array holding the symmetry information if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [checkSymmInfo]
Definition at line 7293 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Finds the largest DD in the population.]
Description [Finds the largest DD in the population. If an order is repeated, it avoids choosing the copy that is in the computed table (it has repeat[i] > 1).]
SideEffects [None]
SeeAlso []
Definition at line 7968 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Generates the random sequences for the initial population.]
Description [Generates the random sequences for the initial population. The sequences are permutations of the indices between lower and upper in the current order.]
SideEffects [None]
SeeAlso []
Definition at line 7793 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Returns the average fitness of the population.]
Description []
SideEffects [None]
SeeAlso [] Function********************************************************************
Synopsis [Performs the crossover between two parents.]
Description [Performs the crossover between two randomly chosen parents, and creates two children, x1 and x2. Uses the Partially Matched Crossover operator.]
SideEffects [None]
SeeAlso []
Definition at line 8138 of file cuddInt.c.
|
static |
|
static |
|
static |
|
static |
Function********************************************************************
Synopsis [Restores the variable order in array by a series of sifts up.]
Description [Restores the variable order in array by a series of sifts up. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 1395 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Selects two parents with the roulette wheel method.]
Description [Selects two distinct parents with the roulette wheel method.]
SideEffects [The indices of the selected parents are returned as side effects.]
SeeAlso []
Definition at line 8258 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Moves one variable up.]
Description [Takes a variable from position x and sifts it up to position x_low; x_low should be less than x. Returns 1 if successful; 0 otherwise]
SideEffects [None]
SeeAlso []
Definition at line 7861 of file cuddInt.c.
Function********************************************************************
Synopsis [Returns the DD to the best position encountered during sifting if there was improvement.]
Description [Otherwise, "tosses a coin" to decide whether to keep the current configuration or return the DD to the original one. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 1301 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Checks termination condition.]
Description [If temperature is STOP_TEMP or there is no improvement then terminates. Returns 1 if the termination criterion is met; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 912 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Updates entry for a subset.]
Description [Updates entry for a subset. Finds the subset, if it exists. If the new order for the subset has lower cost, or if the subset did not exist, it stores the new order and cost. Returns the number of subsets currently in the table.]
SideEffects [None]
SeeAlso []
Definition at line 7201 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Updates the upper bound and saves the best order seen so far.]
Description [Updates the upper bound and saves the best order seen so far. Returns the current value of the upper bound.]
SideEffects [None]
SeeAlso []
Definition at line 6979 of file cuddInt.c.
Function********************************************************************
Synopsis [Swaps two groups.]
Description [Swaps two groups. x is assumed to be the bottom variable of the first group. y is assumed to be the top variable of the second group. Updates the list of moves. Returns the number of keys in the table if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 33423 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Undoes the swap of two groups.]
Description [Undoes the swap of two groups. x is assumed to be the bottom variable of the first group. y is assumed to be the top variable of the second group. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 33530 of file cuddInt.c.
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddSubset0.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 31891 of file cuddInt.c.
CFile***********************************************************************
FileName [cuddZddSetop.c]
PackageName [cudd]
Synopsis [Set operations on ZDDs.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
SeeAlso []
Author [Hyong-Kyoon Shin, In-Ho Moon]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]AutomaticStart
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_zddSubset1.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 31822 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Finds the lower and upper bounds of the group represented by treenode.]
Description [Finds the lower and upper bounds of the group represented by treenode. The high and low fields of treenode are indices. From those we need to derive the current positions, and find maximum and minimum.]
SideEffects [The bounds are returned as side effects.]
SeeAlso []
Definition at line 26860 of file cuddInt.c.
Function********************************************************************
Synopsis [Fixes the ZDD variable group tree after a shuffle.]
Description [Fixes the ZDD variable group tree after a shuffle. Assumes that the order of the variables in a terminal node has not been changed.]
SideEffects [Changes the ZDD variable group tree.]
SeeAlso []
Definition at line 31050 of file cuddInt.c.
Function********************************************************************
Synopsis [Swaps two groups and records the move.]
Description [Swaps two groups and records the move. Returns the number of keys in the DD table in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 27408 of file cuddInt.c.
|
static |
|
static |
Function********************************************************************
Synopsis [Sifts from treenode->low to treenode->high.]
Description [Sifts from treenode->low to treenode->high. If croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the end of the initial sifting. If a group is created, it is then sifted again. After sifting one variable, the group that contains it is dissolved. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 26963 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Sifts one variable up and down until it has taken all positions. Checks for aggregation.]
Description [Sifts one variable up and down until it has taken all positions. Checks for aggregation. There may be at most two sweeps, even if the group grows. Assumes that x is either an isolated variable, or it is the bottom of a group. All groups may not have been found. The variable being moved is returned to the best position seen during sifting. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 27096 of file cuddInt.c.
Function********************************************************************
Synopsis [Determines the best position for a variables and returns it there.]
Description [Determines the best position for a variables and returns it there. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 27588 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts down a variable until it reaches position xHigh.]
Description [Sifts down a variable until it reaches position xHigh. Assumes that x is the bottom of a group (or a singleton). Records all the moves. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 27322 of file cuddInt.c.
Function********************************************************************
Synopsis [Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much.]
Description [Sifts up a variable until either it reaches position xLow or the size of the DD heap increases too much. Assumes that y is the top of a group (or a singleton). Checks y for aggregation to the adjacent variables. Records all the moves that are appended to the list of moves received as input and returned as a side effect. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 27245 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders the children of a group tree node according to the options.]
Description [Reorders the children of a group tree node according to the options. After reordering puts all the variables in the group and/or its descendents in a single group. This allows hierarchical reordering. If the variables in the group do not exist yet, simply does nothing. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 26759 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Shrinks almost empty ZDD subtables at the end of reordering to guarantee that they have a reasonable load factor.]
Description [Shrinks almost empty subtables at the end of reordering to guarantee that they have a reasonable load factor. However, if there many nodes are being reclaimed, then no resizing occurs. Returns 1 in case of success; 0 otherwise.]
SideEffects [None]
Definition at line 30844 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Prepares the ZDD heap for dynamic reordering.]
Description [Prepares the ZDD heap for dynamic reordering. Does garbage collection, to guarantee that there are no dead nodes; and clears the cache, which is invalidated by dynamic reordering.]
SideEffects [None]
Definition at line 30815 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Reorders ZDD variables according to a given permutation.]
Description [Reorders ZDD variables according to a given permutation. The i-th permutation array contains the index of the variable that should be brought to the i-th level. zddShuffle assumes that no dead nodes are present. The reordering is achieved by a series of upward sifts. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 30939 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Moves one ZDD variable up.]
Description [Takes a ZDD variable from position x and sifts it up to position xLow; xLow should be less than or equal to x. Returns 1 if successful; 0 otherwise]
SideEffects [None]
SeeAlso []
Definition at line 31014 of file cuddInt.c.
AutomaticStart
Function********************************************************************
Synopsis [Swaps any two variables.]
Description [Swaps any two variables. Returns the set of moves.]
SideEffects [None]
SeeAlso []
Definition at line 30366 of file cuddInt.c.
|
static |
AutomaticStart
Function********************************************************************
Synopsis [Visits the group tree and reorders each group.]
Description [Recursively visits the group tree and reorders each group in postorder fashion. Returns 1 if successful; 0 otherwise.]
SideEffects [None]
Definition at line 26675 of file cuddInt.c.
|
static |
Function********************************************************************
Synopsis [Comparison function used by qsort.]
Description [Comparison function used by qsort to order the variables according to the number of keys in the subtables. Returns the difference in number of keys between the two variables being compared.]
SideEffects [None]
|
static |
Function********************************************************************
Synopsis [Replaces variables with constants if possible (part of canonical form).]
Description []
SideEffects [None]
SeeAlso []
Definition at line 31961 of file cuddInt.c.
|
static |
CFile***********************************************************************
FileName [cuddAddIte.c]
PackageName [cudd]
Synopsis [ADD ITE function and satellites.]
Description [External procedures included in this module:
Internal procedures included in this module:
Static procedures included in this module:
]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
|
static |
CFile***********************************************************************
FileName [cuddZddGroup.c]
PackageName [cudd]
Synopsis [Functions for ZDD group sifting.]
Description [External procedures included in this file:
Internal procedures included in this file:
Static procedures included in this module:
]
Author [Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
|
static |
CFile***********************************************************************
FileName [cuddGenetic.c]
PackageName [cudd]
Synopsis [Genetic algorithm for variable reordering.]
Description [Internal procedures included in this file:
Static procedures included in this module:
The genetic algorithm implemented here is as follows. We start with the current DD order. We sift this order and use this as the reference DD. We only keep 1 DD around for the entire process and simply rearrange the order of this DD, storing the various orders and their corresponding DD sizes. We generate more random orders to build an initial population. This initial population is 3 times the number of variables, with a maximum of 120. Each random order is built (from the reference DD) and its size stored. Each random order is also sifted to keep the DD sizes fairly small. Then a crossover is performed between two orders (picked randomly) and the two resulting DDs are built and sifted. For each new order, if its size is smaller than any DD in the population, it is inserted into the population and the DD with the largest number of nodes is thrown out. The crossover process happens up to 50 times, and at this point the DD in the population with the smallest size is chosen as the result. This DD must then be built from the reference DD.]
SeeAlso []
Author [Curt Musfeldt, Alan Shuler, Fabio Somenzi]
Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]
1.8.13